[GHC] #9108: GADTs and pattern type annotations?

[GHC]

#9108: GADTs and pattern type annotations?
------------------------------------+-------------------------------------
       Reporter:  edsko             |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.8.2
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 Consider

 {{{
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE KindSignatures #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ScopedTypeVariables #-}

 import Data.Tagged

 data Sing (xs :: [k]) where
   SNil  :: Sing '[]
   SCons :: SingI xs => Sing (x ': xs)

 class SingI (a :: [k]) where
   sing :: Sing a

 instance SingI '[] where
   sing = SNil

 instance SingI xs => SingI (x ': xs) where
   sing = SCons

 lengthSing :: forall (xs :: [k]). SingI xs => Tagged xs Int
 lengthSing = case sing :: Sing xs of
   SNil -> Tagged 0
   (SCons :: Sing (x ': xs')) -> Tagged (1 + untag (lengthSing :: Tagged
 xs' Int))
 }}}

 This gives a type error:

 {{{
     Could not deduce (xs ~ (x : xs'))
     from the context (SingI xs)
       bound by the type signature for
                  lengthSing :: SingI xs => Tagged xs Int
       at Bug.hs:23:15-59
       ‘xs’ is a rigid type variable bound by
            the type signature for lengthSing :: SingI xs => Tagged xs Int
            at Bug.hs:23:22
     Expected type: Sing xs
       Actual type: Sing (x : xs')
 }}}

 But once we pattern match on the `SCons` we know that `xs ~ x ': xs'` for
 some `x`, `xs'`, and we should be able to bring them into scope.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9108>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler