id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc,os,architecture,failure,testcase,blockedby,blocking,related,differential
7352,this type signature in a case alternative does not typecheck and requires ScopedTypeVariables,atnnn,atnnn,"In the following code, E and F are similar data types
{{{
{-# LANGUAGE PolyKinds, DataKinds, GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
data T a = T
data E a where
E :: T a -> E '[a]
data F a where
F :: T a -> F a
test1 = case E T :: E '[True] of
E (T::T True) -> ()
test2 = case F T of
F (T::T True) -> ()
test3 = case E T of E (T::T True) -> ()
}}}
test1 compiles fine with a type signature on E T
test2 compiles fine with no type signature on F T
But test3 does not typecheck, it causes this error with 7.6.1
{{{
Couldn't match kind `Bool' with `Bool'
Expected type: a
Actual type: a0
Kind incompatibility when matching types:
a0 :: Bool
a :: Bool
In the pattern: E (T :: T True)
In a case alternative: E (T :: T True) -> ()
}}}
And this error with current HEAD
{{{
Could not deduce (a ~ 'True)
from the context ((':) Bool a0 ('[] Bool) ~ (':) Bool a ('[] Bool))
bound by a pattern with constructor
E :: forall (k :: BOX) (a :: k). T k a -> E k ((':) k a ('[] k)),
in a case alternative
at /home/atnnn/work/bug.hs:20:3-15
`a' is a rigid type variable bound by
a pattern with constructor
E :: forall (k :: BOX) (a :: k). T k a -> E k ((':) k a ('[] k)),
in a case alternative
at /home/atnnn/work/bug.hs:20:3
Expected type: T Bool 'True
Actual type: T Bool a
In the pattern: T :: T True
In the pattern: E (T :: T True)
In a case alternative: E (T :: T True) -> ()
}}}
Additionally, removing the ScopedTypeVariables pragma causes an error for each test
{{{
Illegal type signature: `T True'
Perhaps you intended to use -XScopedTypeVariables
In a pattern type-signature
}}}
But there are no visible type variables in the type signatures",bug,closed,normal,,Compiler (Type checker),7.6.1,invalid,,,Unknown/Multiple,Unknown/Multiple,None/Unknown,,,,,