[GHC] #13408: Consider inferring a higher-rank kind for type synonyms

[GHC]

#13408: Consider inferring a higher-rank kind for type synonyms
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  feature request   |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.0.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 goldfire):

 It's just a little twiddling! How hard could it be? :)

 You ask good questions. But your first guesses are off:

 - `tcInferInst` is the right notional idea, but not a function you would
 actually use here.
 - `getInitialKind` looks at the "left-hand side" of a type declaration and
 invents a skeleton for the type's kind. (Example: from `data T a (b ::
 Type -> Type) c`, it guesses `T :: kappa1 -> (Type -> Type) -> kappa2 ->
 Type` for fresh unification variables `kappa1` and `kappa2`.) Because you
 don't need to guess the kind, it's not what you want here.

 What you need to do is to bring the type variables on the LHS into scope
 (with either guessed or provided kinds), kind-check the RHS, and then say
 that the LHS's kind is the same as the RHS's. Here is some direction to
 how to do so:

 - Have a special case in `kcTyClGroup` that detects a single type synonym.
 Type synonyms cannot be recursive, so we don't have to worry about that.
 (Or maybe we do, because we detect recursion in type synonyms later,
 perhaps? If that's the case, the renamer may want to either reject
 recursive type synonyms or remember the recursiveness using a new field in
 the AST.)
 - `kcLHsQTyVars` brings the LHS tyvars into scope, with appropriate kinds.
 Claim that the type does ''not'' have a CUSK. (Even if it ''does'' have a
 CUSK, CUSKness can matter only with recursion.)
 - `tcLHsType` does a nice job of checking the type itself -- but you'll
 need only the kind here, not the type.
 - You'll need to skolemise and quantify, much like the main branch of
 `kcTyClGroup`.

 Does that give enough guidance?

 I do think that, actually, we can do better here. The plan above would
 still have GHC take two passes over these special type synonyms, when
 really we can do it in one pass. But the infrastructure isn't set up for
 that, so it would take a more significant refactoring. Still I think the
 plan above is an improvement over the status quo.

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