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