Re: [GHC] #14111: strange error when using data families with levity polymorphism and unboxed sums and data families

23 Jul 2018

      #14111: strange error when using data families with levity polymorphism and unboxed
sums and data families
-------------------------------------+-------------------------------------
        Reporter:  carter            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:  13737             |             Blocking:
 Related Tickets:  #14457            |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Aha! Thank you goldfire, that plan works beautifully. With that, I am able
 to write a patch (based off of comment:14, and applied on top of
 Phab:D4974) which fixes the original program. Woohoo!

 ...there's one gotcha, though. Since we're now straight-up using
 `unifyType` in `tcConDecl`, some of the error messages degrade in quality.
 One example is in the `T12087` test case, which currently gives a rather
 informative error message:

 {{{
 T12087.hs:6:3: error:
     • GADT constructor type signature cannot contain nested ‘forall’s or
 contexts
       Suggestion: instead use this type signature:
         MkF1 :: forall a. (Ord a, Eq a) => a -> F1 a
     • In the definition of data constructor ‘MkF1’
       In the data type declaration for ‘F1’
 }}}

 But after my patch, this turns into:

 {{{
 T12087.hs:6:3:
      Couldn't match expected type ‘F1 a0’
                   with actual type ‘Eq a1 => a1 -> F1 a1’
      In the definition of data constructor ‘MkF1’
 }}}

 Which kind of sucks. The reason this happens is because the `GADT
 constructor type signature cannot contain nested ‘forall’s or contexts`
 error is emitted in `checkValidDataCon`, which comes //after// `tcConDecl`
 (currently, GHC assumes that `tcConDecl` will ignore ill formatted data
 constructors like these, and let `checkValidDataCon` catch them
 afterwards).

 I'm not quite sure how to deal with this. Perhaps we should carve out that
 particular check from `checkValidDataCon` and put it before the call to
 `unifyType` in `tcConDecl`? It's a bit arbitrary, but I think it would
 address the issue. As an added bonus, it might fix #11384, since
 performing this check earlier might give GHC a chance to spot an improper
 return type before kind-checking occurs.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14111#comment:21
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler