this type signature in a case alternative does not typecheck and requires ScopedTypeVariables
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
Trac metadata
Trac field | Value |
---|---|
Version | 7.6.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |