GADTs and pattern type annotations?
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.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |