Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,249
    • Issues 5,249
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 582
    • Merge requests 582
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #2206
Closed
Open
Issue created Apr 10, 2008 by Simon Peyton Jones@simonpjDeveloper

GADT pattern match with non-rigid return type

Chris Casinghino (ccasin@seas.upenn.edu) 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!

Trac metadata
Trac field Value
Version 6.8.2
Type Bug
TypeOfFailure OtherFailure
Priority normal
Resolution Unresolved
Component Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC ccasin@seas.upenn.edu
Operating system Unknown
Architecture Unknown
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking