Associated type synonyms not fully simplified in GHCi

The following code works as expected when compiled in GHC, or even when loaded into GHCi and run with "main":

{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleContexts #-}

data Z = Z
data S n = S n

class Peano n where
    mkPeano :: n
    toInt   :: n -> Int

instance Peano Z where
    mkPeano = Z
    toInt Z = 0
instance Peano n => Peano (S n) where
    mkPeano = S mkPeano
    toInt (S n) = 1 + toInt n

class (Peano a, Peano b, Peano (Sum a b)) => BinOp a b where
    type Sum a b
instance BinOp Z Z where type Sum Z Z = Z
instance Peano a => BinOp Z (S a) where type Sum Z (S a) = S a
instance Peano a => BinOp (S a) Z where type Sum (S a) Z = S a
instance BinOp a b => BinOp (S a) (S b) where
    type Sum (S a) (S b) = S (S (Sum a b))

add :: BinOp a b => a -> b -> Sum a b
add _ _ = mkPeano

main = do
  print $ toInt $ add Z $ add Z Z

However, if the contents of main is typed at the GHCi prompt (toInt $ add Z $ add Z Z), it complains that No instance for (BinOp Z (Sum Z Z)) arising from a use of add' at :1:8-12`. Evidently it stops short before evaluating that Sum Z Z = Z and therefore BinOp Z Z is in fact an instance. This is the case both in 6.8.3 as well as 6.10.0.20080921.

If "seq 1" is inserted, as in "toInt $ seq 1 $ add Z $ add Z Z", then GHCi again behaves consistently with GHC. This is therefore a workaround, albeit inconvenient.

Trac metadata

Trac field	Value
Version	6.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	GHCi
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture