Opened 6 years ago

Closed 5 years ago

Last modified 4 years ago

#2206 closed bug (fixed)

GADT pattern match with non-rigid return type

Reported by: simonpj Owned by: simonpj
Priority: normal Milestone: 6.10 branch
Component: Compiler Version: 6.8.2
Keywords: Cc: ccasin@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Difficulty: Unknown
Test Case: gadt-escape1 Blocked By:
Blocking: Related Tickets:

Description

Chris Casinghino (ccasin@…) writes: I've been playing with some GADT stuff with Stephanie Weirich and I think we've found a bug in GHC at the intersection of GADTs and
existentials. The HEAD version gives a type error when :loading this
program into ghci:

> data ExpGADT t where
>   ExpInt :: Int -> ExpGADT Int
>
> data Hidden = forall t . Hidden (ExpGADT t) (ExpGADT t)
>
> hval = Hidden (ExpInt 0) (ExpInt 1)
>
> weird = case (hval :: Hidden) of Hidden (ExpInt _) a -> a

ghc thinks the existential type variable has escaped:

test.hs:11:33:
     Inferred type is less polymorphic than expected
       Quantified type variable `t' escapes
     When checking an existential match that binds
         a :: ExpGADT t
     The pattern(s) have type(s): Hidden
     The body has type: ExpGADT t
     In a case alternative: Hidden (ExpInt _) a -> a
     In the expression:
         case (hval :: Hidden) of Hidden (ExpInt _) a -> a

According to the rules in the wobbly types paper, this should
typecheck and weird should be given the wobbly type (ExpGADT Int).

Perhaps this type error is an intentional deviation from the spec? If
so, I'd love to know what implementation issues brought about the
change. If not, I suppose it's a bug.

Everything works fine if we add a type annotation for weird.
Strangely, in ghc 6.8.2, the program is accepted when :loaded, but if
after doing so I copy:

   let weird2 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a

into ghci, I get an error.

Anyway, I thought I should point out this discrepancy. I hope it's
helpful!

Change History (6)

comment:1 Changed 6 years ago by chak

The implementation of GADTs in the development version of GHC recently changed completely. It's now based on a combination of implication constraints and type equality constraints. I believe what happens is the following. In the case alternative, we have a :: ExpGADT t together with an equality constraint t ~ Int. So, GHC is right to claim that t escapes its scope; it does albeit escape in conjunction with the equality t ~ Int.

At the moment, GHC does not properly enforce the constraints on type rigidity, but in the course of investigating the interaction between GADTs and type families, we came to the conclusion that we need to require not only that the type of the scrutinee of a GADT match is rigid, but also its return type. Hence, the example code should indeed be rejected, but ideally the error message should point out that the return type should be rigid (instead of the somewhat unhelpful message produced currently).

comment:2 Changed 6 years ago by simonpj

  • Owner set to simonpj

Indeed.

I have a fix for 2206 in my tree (testing now), so I'll take this. However, the whole rigidity thing is shaky (ha ha) at the moment, because boxy types and rigid types are mixed up. We need to take a new look as the dust settles on type equalities.

Simon

comment:3 Changed 6 years ago by igloo

  • Milestone set to 6.10 branch

comment:4 Changed 6 years ago by simonmar

  • Architecture changed from Unknown to Unknown/Multiple

comment:5 Changed 6 years ago by simonmar

  • Operating System changed from Unknown to Unknown/Multiple

comment:6 Changed 5 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed

Indeed GHC 6.10 now (correctly) reports

$ ghc -c T2206.hs

T2206.hs:12:51:
    GADT pattern match with non-rigid result type `t'
      Solution: add a type signature
    In a case alternative: Hidden (ExpInt _) a -> a
    In the expression:
        case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }
    In the definition of `weird':
        weird = case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }

which seems like a decent error message. So I'll close this one.

Simon

Note: See TracTickets for help on using tickets.