[GHC] #7766: equality constraints exposed by patterns mess up constraint inference

[Simon Peyton-Jones]

You probably need
  do { (case .... of ...) :: IO ()
     ; return () }

It's not a bug, in other words.  The "modular type inference with local constraints" paper is a good reference here.

Simon

| -----Original Message-----
| From: Gabor Greif [mailto:ggreif at gmail.com]
| Sent: 13 March 2013 15:05
| To: ghc-devs at haskell.org; Simon Peyton-Jones
| Cc: ghc-tickets at haskell.org
| Subject: Re: [GHC] #7766: equality constraints exposed by patterns mess
| up constraint inference
| 
| Hi Simon,
| 
| okay, I see how a type signature will help in that case, but it is
| unclear where to add one in this (even simpler) example:
| 
| 
| {-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
| 
| data Nat = S Nat | Z
| 
| data Nat' (n :: Nat) where
|   S' :: Nat' n -> Nat' (S n)
|   Z' :: Nat' Z
| 
| main :: IO ()
| main = do case S' Z' of
|            (S' Z') -> putStrLn "yep" -- see error message below...
|            -- _ -> putStrLn "yep" -- works!
|           return ()
| 
| {-
| [1 of 1] Compiling Main             ( pr7766.hs, pr7766.o )
| 
| pr7766.hs:11:23:
|     Couldn't match type `a0' with `()'
|       `a0' is untouchable
|         inside the constraints (n ~ 'Z)
|         bound by a pattern with constructor
|                    Z' :: Nat' 'Z,
|                  in a case alternative
|         at pr7766.hs:11:16-17
|     Expected type: IO a0
|       Actual type: IO ()
|     In the return type of a call of `putStrLn'
|     In the expression: putStrLn "yep"
|     In a case alternative: (S' Z') -> putStrLn "yep"
| -}
| 
| 
| Can we reopen the PR with this test? (Distilled from real code I have
| and which fails as of recently.)
| 
| Thanks and cheers,
| 
|     Gabor
| 
| On 3/13/13, GHC <cvs-ghc at haskell.org> wrote:
| > #7766: equality constraints exposed by patterns mess up constraint
| > inference
| > ----------------------------------------+-----------------------------
| > ----------------------------------------+------
| >   Reporter:  heisenbug                  |          Owner:
| >       Type:  bug                        |         Status:  closed
| >   Priority:  normal                     |      Milestone:
| >  Component:  Compiler                   |        Version:  7.7
| > Resolution:  invalid                    |       Keywords:
| >         Os:  Unknown/Multiple           |   Architecture:
| Unknown/Multiple
| >    Failure:  GHC rejects valid program  |     Difficulty:  Unknown
| >   Testcase:                             |      Blockedby:
| >   Blocking:                             |        Related:
| > ----------------------------------------+-----------------------------
| > ----------------------------------------+------
| > Changes (by simonpj):
| >
| >   * status:  new => closed
| >   * difficulty:  => Unknown
| >   * resolution:  => invalid
| >
| >
| > Comment:
| >
| >  This is by design.   Type inference in the presence of GADTs is
| tricky!
| >
| >  If you give the signature `main :: IO ()` it works fine.  But here
| > you are  asking GHC to ''infer'' the type of `main`.  (Remember,
| > Haskell doesn't  insist on `IO ()`; the `main` function can have type
| > `IO Char`.)
| >
| >  Becuase you are pattern matching against GADTs there are equalities
| > in  scope, so GHC declines to contrain the type of `main`.  In this
| > particular  case there is only one answer, but that's very hard to
| > figure out, so we  fail conservatively.
| >
| >  Bottom line: use type signatures when pattern matching on GADTs.
| >
| >  Simon
| >
| > --
| > Ticket URL:
| > <http://hackage.haskell.org/trac/ghc/ticket/7766#comment:1>
| > GHC <http://www.haskell.org/ghc/>
| > The Glasgow Haskell Compiler
| >