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 |