#9273: TypeNats and record syntax don't compile -------------------------------------+------------------------------------- Reporter: br1 | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.2 checker) | Operating System: Unknown/Multiple Keywords: | Type of failure: GHC rejects Architecture: Unknown/Multiple | valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | -------------------------------------+------------------------------------- {{{ #!haskell 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 {{{ #!haskell data SNat :: Nat -> * where SNatZ :: SNat 0 SNatS :: SNat n -> SNat (n+1) }}} works. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9273 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler