[GHC] #15057: Lint types created by newFamInst

[GHC]

#15057: Lint types created by newFamInst
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  closed
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.4.1
      Resolution:  fixed             |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:  #15012            |  Differential Rev(s):  Phab:D4611
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Thanks for doing this, but I don't think it's quite right yet.

 As you have it, we

 * Expand type synonyms usually
 * But not when calling from `newFamInst`

 But that isn't what we want.
 Consider these definitions:
 {{{
 type S1 x = Int
 type S2 x = x Int
 }}}
 In regular Core, if `a` is not in scope, it'd be bad to
 have a type `S1 a`. Likewise `S2 (Int Int)` would be bad (kind error).
 With your patch this will be missed.

 Moreover, in `newFamInst`, it's ok to have a RHS with a
 partially-applied type synonym like `S2 S1`.  But I think your patch
 will reject it.

 What we want is something like this:

 * In a type-synonym application `S t1 .. tn`:
   1. Expand the synonym and lint the result
   2. But also lint `t1..tn` independently, to find any out-of-scope
 variables or kind errors

 The trouble is that in `t1..tn` we are allowed to have an un-saturated
 synonym application, ''but only at top level''.  For example, suppose
 {{{
 }}}
 Then `S2 S1` is fine, but `S2 (Maybe S1)` is not.  Of course, the latter
 is detected in step (1).  But it won't be detected in `S1 (Maybe S1)`.   I
 think I don't care about that; un-saturated synonyms in a phantom
 argument.

 So that would make the rule be as follows:

 * Have a flag report-unsat-syns
 * In a type-synonym application `S t1 .. tn`:
   1. If report-unsat-syns is on, and `S` has arity more than n, report an
 unsaturated synonym
   2. If report-unsat-syns is on, expand the synonym and lint the result
   3. Regardless of report-unsat-syns, lint `t1..tn` independently with
 report-unsat-syns off,
      to find any out-of-scope variables or kind errors
 * Switch on report-unsat-syns for the arguments of `AppTy` and `TyConApp`
 with non-synonym type constructor.

 There is some duplicated work here: for non-phantom arguments, if report-
 unsat-syns is on, all the work of (3) is done by (2).  So you could do (3)
 only for phantom arguments.

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