[GHC] #12087: Inconsistency in GADTs?

[GHC]

#12087: Inconsistency in GADTs?
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  task              |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.1
      Resolution:                    |             Keywords:  GADTs
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #11540            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: RyanGlScott (added)
 * status:  closed => new
 * resolution:  invalid =>
 * related:   => #11540


Comment:

 I disagree that this not "valid" Haskell. It's certainly not //standard//
 Haskell, but I don't see why it ought to be rejected. Perhaps one day
 after #11540 is fixed, we'll need some extra language extension enabled to
 use this feature, but I think GHC is more than capable of handling such a
 thing.

 For background context: the structure of GADT type signatures are
 currently validity checked in a rather simple-minded way in
 [http://git.haskell.org/ghc.git/blob/86abe0e03f6cc2392758d6b45390177d44896113:/compiler/hsSyn/HsDecls.hs#l1189
 gadtDeclDetails]. It splits apart a single `forall` with `splitLHsSigmaTy`
 and checks if the return type is of the form `T a_1 ... a_n`, where `T` is
 the GADT tycon. But since there's nested sigma types here, GHC mistakenly
 believes that the return type is `Eq a => a -> F a`, which is bad news.

 I think it would be possible to tweak this check to accommodate nested
 foralls, though. Essentially, I think we'd need to create a version of
 [http://git.haskell.org/ghc.git/blob/86abe0e03f6cc2392758d6b45390177d44896113:/compiler/typecheck/TcType.hs#l1420
 tcSplitNestedSigmaTys] that works over `LHsType` instead of `Type`, and
 replace the use of `splitLHsSigmaTy` with that in `gadtDeclDetails`. Then
 we'd typecheck `MkF` as if it had the type `forall a. (Ord a, Eq a) => a
 -> F a`.  This isn't exactly what the user //wrote//, but it's equivalent
 and serviceable.

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