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

[Gabor Greif]

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
>