TypeNats and record syntax don't compile
data SNat :: Nat -> * where
SNatZ :: SNat 0
SNatS :: {sNatPred :: SNat n} -> SNat (n+1)
gives error
rec_gadt_nat.hs:13:13:
Could not deduce (n1 ~ n)
from the context ((n + 1) ~ (n1 + 1))
bound by a pattern with constructor
SNatS :: forall (n :: Nat). SNat n -> SNat (n + 1),
in an equation for ‘sNatPred’
at rec_gadt_nat.hs:13:13-20
‘n1’ is a rigid type variable bound by
a pattern with constructor
SNatS :: forall (n :: Nat). SNat n -> SNat (n + 1),
in an equation for ‘sNatPred’
at rec_gadt_nat.hs:13:13
‘n’ is a rigid type variable bound by
the type signature for sNatPred :: SNat (n + 1) -> SNat n
at rec_gadt_nat.hs:13:13
Expected type: SNat n
Actual type: SNat n1
Relevant bindings include
sNatPred :: SNat n1 (bound at rec_gadt_nat.hs:13:13)
sNatPred :: SNat (n + 1) -> SNat n (bound at rec_gadt_nat.hs:13:13)
In the expression: sNatPred
In an equation for ‘sNatPred’:
sNatPred (SNatS {sNatPred = sNatPred}) = sNatPred
while
data SNat :: Nat -> * where
SNatZ :: SNat 0
SNatS :: SNat n -> SNat (n+1)
works.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |