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

13 Mar 2013

      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  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

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

Gabor Greif