<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>