Opened 5 years ago

Closed 5 years ago

#6075 closed bug (invalid)

Incorrect interpretation of scoped type variable declaration in GADT pattern match

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.5
Keywords: ScopedTypeVariables GADTs 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:


Consider the following code:

{-# LANGUAGE GADTs, FlexibleInstances, ScopedTypeVariables #-}

class FromThinAir a where
  create :: a
instance FromThinAir Int where
  create = 42
instance FromThinAir [Char] where
  create = "Poof!"

data GADT a where
  GInt :: GADT Int
  GArrow :: (FromThinAir a, Show a) => GADT (a -> b)

data NotGADT where
  NInt :: Int -> NotGADT
  NArrow :: (FromThinAir a, Show a) => (a -> b) -> NotGADT

dumb :: NotGADT -> String
dumb g = case g of
  NInt _ -> show (create :: Int)
  NArrow (f :: (a -> b)) -> show (create :: a)

dumber :: GADT a -> String
dumber g = case g of
  GInt -> show (create :: Int)
  (GArrow :: GADT (a -> b)) -> show (create :: a)

The function dumb compiles just fine. The function dumber does not. The problem appears to be that GHC interprets the type signature on GArrow as a type signature that applies to all cases, or (equivalently) applies to g. In dumb, however, the type signature is applied to a variable, not the constructor, and GHC does the right thing.

Note that the FromThinAir class simply sets the stage for the bug. I don't believe it's an integral part of it all.

This was tested on 7.5.20120426.

Change History (1)

comment:1 Changed 5 years ago by simonpj

difficulty: Unknown
Resolution: invalid
Status: newclosed

The errror mesage (with GHC 7.4) is this:

    Couldn't match type `a -> b' with `Int'
    Inaccessible code in
      a pattern with constructor GInt :: GADT Int, in a case alternative
    In the pattern: GInt
    In a case alternative: GInt -> show (create :: Int)

And that seems right to me. Consider the semantics of pattern matching in the Haskell report. To 3.17.2 add the informal rule

  • Matching the pattern (p :: ty) against a value v requires v to have type ty (or else a static error results), and then matches p against v.

To 3.17.3 add a rule for type signatures

case v of { (p :: type) -> e1; _ -> e2 }
case (v :: type) of { p -> e1; _ -> e2 }

(This rule does not take account of bringing lexical type variables into scope, but is otherwise right.)

In short, patterns are matched outside in, so we don't get to see that the pattern has type GADT (a->b) until after we've matched GArrow, but the type signature applies before.

Note: See TracTickets for help on using tickets.