Opened 6 years ago

Closed 6 years ago

#7352 closed bug (invalid)

this type signature in a case alternative does not typecheck and requires ScopedTypeVariables

Reported by: atnnn Owned by: atnnn
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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

Change History (4)

comment:1 Changed 6 years ago by atnnn

Owner: set to atnnn

comment:2 Changed 6 years ago by atnnn

comment:3 Changed 6 years ago by atnnn

Turning on -ddump-tc-trace makes GHC panic on the declaration of E

{-# LANGUAGE PolyKinds, DataKinds, GADTs #-}

data T a = T

data E a where
  E :: T a -> E '[a]
tc_lhs_type:
  a
  Expected kind: k_af0
lk1 a
lk2 a AThing k_aeU
checkExpectedKind
  a
  k_aeU
  Expected kind: k_af0
writeMetaTyVar k_aeY := k_af0
checkExpectedKindghc-stage2: panic! (the 'impossible' happened)
  (GHC version 7.7.20121020 for x86_64-unknown-linux):
        AThing evaluated unexpectedly tcTyVar a{tv aeN}

comment:4 Changed 6 years ago by atnnn

Resolution: invalid
Status: newclosed

This is not a bug, just the normal behaviour of GADTs

{-# LANGUAGE GADTs #-}

data G a where
  G :: {unG :: a} -> G [a]

test4 (G True) = ()

test4 fails with

    Could not deduce (a ~ Bool)
    from the context (t ~ [a])

Here is a workaround that works

test5 g | True <- unG g = ()
Note: See TracTickets for help on using tickets.