[GHC] #9273: TypeNats and record syntax don't compile

[GHC]

#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