[GHC] #14451: Type synonym of type family causes error, error jumps to (fairly) unrelated source location

[GHC]

#14451: Type synonym of type family causes error, error jumps to (fairly) unrelated
source location
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:  TypeInType
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 I don't think this is #11203.   Here's what I think is happening

 * `Apply`, `Comp`, and `OO` (which I will use instead of the unicode dot
 symbol) are mutually
 recursive, and so are kind-checked together.

 * The first two have CUSKs and so `getInitialKinds` gives them polykinds,
 thus
 {{{
 kcTyClGroup: initial kinds
   [r1 :-> ATcTyCon Apply :: forall a b. (a ~> b) -> a -> b,
    r2 :-> ATcTyCon Comp :: forall k1 k2 k.
                            (k1 ~> k) -> (k2 ~> k1) -> k2 -> k,
    r4 :-> ATcTyCon OO :: k_aYg[tau:1] -> k_aYh[tau:1] -> k_aYi[tau:1]]
 }}}
   Good so far.

 * But then pathetically, we run over all three declarations, gathering
 constraints
   on the kind variables in `OO`. In the end we make `OO` insufficiently
 polymorphic,
   giving it kind
 {{{
   OO :: forall b. (b ~> b) -> b -> b
 }}}
   whereas it should have kind
 {{{
   OO :: forall a b. (a ~> b) -> a -> b
 }}}
   That's stupid: `OO`'s kind should obviously be the same as `Apply`'s

 What we ''should'' do is exactly what we do for value declarations:

 * Take the SCC (the group of three declarations)
 * Remove edges that point to type constructors that have a CUSK
 * Do a new SCC on this thinned-out graph.
 * Now `OO` will be first, in a SCC by itself, because `Apply` and `Comp`
 depend on it, but not vice versa (after removing those edges)
 * Now kind-check each smaller SCC one by one, generalising each in turn.

 For bindings you can see the extra SCC analysis being done in
 `TcBinds.tc_group`.

 So all we have to do is to replicate this logic for types.  Fiddly,
 perhaps, but not difficult.

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