Hi, 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 plusComm (SS m') n' = _ GHC tells me that I have a single hole in the file with type 'S (m1 :+: n) :~: (n :+: 'S m1) 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 plusComm (SS m') n' = substR (plusComm m' n') _ GHC tells me that the remaining hole now has type 'S (m1 :+: n) :~: (m1 :+: n) which seems completely incorrect to me. Shouldn't this hole have type 'S (n :+: m1) :~: (n :+: S m1) ? Can anybody give any clues as to what is happening? Thanks, Dominic {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} module MinimumExample where data (:~:) (a :: k) (b :: k) where Refl :: a :~: a substR :: a :~: b -> f a -> f b substR Refl x = x substL :: a :~: b -> f b -> f a substL Refl x = x cong :: a :~: b -> f a :~: f b cong Refl = Refl data Nat where Z :: Nat S :: Nat -> Nat data NatS (m :: Nat) where ZS :: NatS Z SS :: NatS m -> NatS (S m) type family (:+:) (m :: Nat) (n :: Nat) :: Nat where Z :+: n = n (S m) :+: n = S (m :+: n) plusZRightNeutral :: NatS m -> (m :+: Z) :~: m plusZRightNeutral ZS = Refl plusZRightNeutral (SS m') = cong (plusZRightNeutral m') plusComm :: NatS m -> NatS n -> (m :+: n) :~: (n :+: m) plusComm ZS n' = substL (plusZRightNeutral n') Refl -- everything seems correct here plusComm (SS m') n = _ -- but things look completely incorrect, here -- plusComm (SS m') n' = substR (plusComm m' n') _