[GHC] #14419: Check kinds for ambiguity

[GHC]

#14419: Check kinds for ambiguity
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                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 goldfire):

 Simon, Ryan, and I had a confab about all this. We discovered several new
 insights:

 * The subkinding relationship is different than the subtyping
 relationship. Definition: `t1 <= t2` iff there exists a way to transform a
 `t1` into a `t2`. That is, there exists an expression of type `t2` with a
 `t1`-shaped hole. (Note that `tcSubType` and friends return an
 `HsWrapper`, which is precisely an expression with a hole in it.) In
 kinds, however, the expression language is different: it is the language
 of types, not terms. And, critically, there is no type-level lambda. Thus,
 the expression-with-a-hole is more limited, meaning fewer pairs of kinds
 are in the subkinding relationship.

 * To wit, the subkinding relationship has these rules:

 {{{
 ----------- Refl
 t <= t

 t[t'/a] <= s
 ----------- Inst
 forall a. t   <=   s
 }}}

     And that's it. (The `t`s above might be polytypes.) This is in
 contrast to the traditional subtyping relationship (e.g. bottom of Fig. 5
 from the [https://www.microsoft.com/en-us/research/wp-
 content/uploads/2016/02/putting.pdf Practical Type Inference] paper),
 which has rules for skolemization and contravariance of functions.

 * An ambiguity check is really a check to see whether a definition can be
 used unambiguously, without the need for visible type application. In
 terms, this notion is equivalent to a reflexive sub-type check. That is,
 `t` is unambiguous iff `t <= t`. However, this is ''not'' true in kinds.
 To wit, if `F` is a type family, then `forall a. F a -> Type` is a subkind
 of itself according to the relation above. We thus can't use a subkinding
 check to implement kind-level ambiguity.

 * The subkinding relation is implemented in `TcHsType.checkExpectedKind`
 and friends, which checks a type-checked type against an expected kind.

 We have two tasks:

 1. Document `checkExpectedKind` and friends in light of the observation
 that they are computing a subkinding relation. This is a simpler way to
 understand those functions.

 2. Write a kind-level ambiguity check. This check can simply look at a
 kind to ensure that all quantified kind variables appear under a sequence
 of injective type constructors. (That is, for each quantified variable,
 check that there exists a path from the root of the kind tree to an
 occurrence of the variable passing through only injective types.) I
 believe we had such a check for types, once upon a time, but removed it
 when Simon discovered the relationship between ambiguity and the subtyping
 relation.

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