#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