[GHC] #10729: Type inference in GADT pattern matches

[GHC]

#10729: Type inference in GADT pattern matches
-------------------------------------+-------------------------------------
        Reporter:  mniip             |                   Owner:
            Type:  bug               |                  Status:  closed
        Priority:  normal            |               Milestone:
       Component:  Compiler (Type    |                 Version:  7.11
  checker)                           |
      Resolution:  invalid           |                Keywords:
Operating System:  Unknown/Multiple  |            Architecture:
 Type of failure:  GHC rejects       |  Unknown/Multiple
  valid program                      |               Test Case:
      Blocked By:                    |                Blocking:
 Related Tickets:                    |  Differential Revisions:
-------------------------------------+-------------------------------------
Changes (by rwbarton):

 * status:  new => closed
 * resolution:   => invalid


Comment:

 Replying to [ticket:10729 mniip]:
 > When pattern matching against GADT constructors, GHC seems to have
 issues with inferring the type of the resulting expression.
 >
 > Minimal example: Assume the datatype:
 >
 > {{{
 > data D a where D :: D ()
 > }}}
 > A simple function that pattern matches on it:
 > {{{
 > a D = ()
 > }}}
 > It is expected to have type `D a -> ()`

 Why not `a :: D a -> a`? This function definition has no principal type.

 See the very end of the user's guide section
 https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/data-type-
 extensions.html#gadt. The type of the function body is not rigid in your
 example, because you did not specify it with a type annotation, and the
 only information about the type comes from inside a pattern match on a
 refining constructor. It is one of the examples in the linked paper, in
 appendix A.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/10729#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler