#7352: this type signature in a case alternative does not typecheck and requires
ScopedTypeVariables
------------------------------+---------------------------------------------
Reporter: atnnn | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler (Type checker)
Version: 7.6.1 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: None/Unknown | Testcase:
Blockedby: | Blocking:
Related: |
------------------------------+---------------------------------------------
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
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/7352>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
