<div dir="ltr">Hi,<div><br></div><div>I've come across some behaviour in GHC 7.8.2 which seems strange, and may be a bug, but I wish to check before reporting it. Consider the minimum example pasted at the bottom of this message. At the line</div>
<div><br></div><div> plusComm (SS m') n' = _</div><div><br></div><div><div>GHC tells me that I have a single hole in the file with type</div><div><br></div><div> 'S (m1 :+: n) :~: (n :+: 'S m1)</div></div>
<div><br></div><div>which is straightforward to provide, by rewriting with the inductive hypothesis (a recursive call of plusComm) and then some fiddling. However, replacing this line with the refinement</div><div><br></div>
<div> plusComm (SS m') n' = substR (plusComm m' n') _</div><div><br></div><div>GHC tells me that the remaining hole now has type</div><div><br></div><div> 'S (m1 :+: n) :~: (m1 :+: n)<br></div><div><br>
</div><div>which seems completely incorrect to me. Shouldn't this hole have type</div><div><br></div><div> 'S (n :+: m1) :~: (n :+: S m1)<br></div><div><br></div><div>? Can anybody give any clues as to what is happening?</div>
<div><br></div><div>Thanks,</div><div>Dominic</div><div><br></div><div><br></div><div><br></div><div><br></div><div> </div><div><br></div><div><div>{-# LANGUAGE DataKinds #-}</div><div>{-# LANGUAGE GADTs #-}</div><div>{-# LANGUAGE KindSignatures #-}</div>
<div>{-# LANGUAGE PolyKinds #-}</div><div>{-# LANGUAGE TypeFamilies #-}</div><div>{-# LANGUAGE TypeOperators #-}</div><div><br></div><div>module MinimumExample where</div><div><br></div><div> data (:~:) (a :: k) (b :: k) where</div>
<div> Refl :: a :~: a</div><div> </div><div> substR :: a :~: b -> f a -> f b</div><div> substR Refl x = x</div><div> </div><div> substL :: a :~: b -> f b -> f a</div><div> substL Refl x = x</div><div>
</div><div> cong :: a :~: b -> f a :~: f b</div><div> cong Refl = Refl</div><div> </div><div> data Nat where</div><div> Z :: Nat</div><div> S :: Nat -> Nat</div><div> </div><div> data NatS (m :: Nat) where</div>
<div> ZS :: NatS Z</div><div> SS :: NatS m -> NatS (S m)</div><div> </div><div> type family (:+:) (m :: Nat) (n :: Nat) :: Nat where</div><div> Z :+: n = n</div><div> (S m) :+: n = S (m :+: n)</div><div>
</div><div> plusZRightNeutral :: NatS m -> (m :+: Z) :~: m</div><div> plusZRightNeutral ZS = Refl</div><div> plusZRightNeutral (SS m') = cong (plusZRightNeutral m')</div><div> </div><div> plusComm :: NatS m -> NatS n -> (m :+: n) :~: (n :+: m)</div>
<div> plusComm ZS n' = substL (plusZRightNeutral n') Refl</div><div> -- everything seems correct here</div><div> plusComm (SS m') n = _</div><div> -- but things look completely incorrect, here</div><div>
-- plusComm (SS m') n' = substR (plusComm m' n') _</div></div></div>