kind inference (#11203)

[Richard Eisenberg]

Actually, I think I know how to fix the problem with (3) and (4), by unifying the kinds in any KindedTyVars in the tycon's LHsQTyVars with the tyvar kinds in the tycon's kind. I have some preliminary code toward this, and should return to the problem early next week.

(2), on the other hand, is a bit of a mystery how to solve.

Richard

On Dec 11, 2015, at 4:43 PM, Richard Eisenberg <eir at cis.upenn.edu> wrote:

> Hi Simon and other devs,
> 
> I struggled a bit today with some issues around kind inference that I wanted to write down.
> 
> Here are some illuminating test cases, explained below:
> 
> -- useful definition:
> data SameKind :: k -> k -> *
> 
> 1.
> data T (a :: k1) x = MkT (S a ())
> data S (b :: k2) y = MkS (T b ())
> 
> 2.
> data Q (a :: k1) (b :: k2) c = MkQ (SameKind a b)
> 
> 3.
> data D1 = MkD1 (forall p (a :: k). p a -> Int)
> 
> 4.
> data D2 a b = MkD2 (Proxy (a :: Maybe k)) | MkD3 (Proxy (b :: [k])
> 
> 
> (1) should be accepted. But this is rather hard to arrange for, because T and S do not have CUSKs. Their kinds are generalized only after checking the mutually-recursive group. So, to accept this pair, we need to use SigTvs for k1 and k2, to allow them to unify with each other. (This works today.)
> 
> (2) should be rejected. But it is currently accepted, because k1 and k2 are SigTvs, and so they unify with each other.
> 
> (3) should be rejected. I have no idea where that k should be bound. Previously, the k was bound in the forall, but after the wildcards-refactor patch, that's no longer possible. (This is taken from test case ghci/scripts/T7873. HEAD accepts this definition, but produces a bogus tycon.) Note that this was accepted correctly before the wildcards-refactor.
> 
> (4) should be accepted. This demonstrates that k can be introduced in constructors but scopes over the entire definition. The difference with case (3) is that (4) has type variables whose kinds mention k, whereas (3) does not.
> 
> How should we arrange for all of this behavior? As stated in #11203, I think the use of SigTvs in PolyKinds is highly suspect. I have no good ideas here, though.
> 
> In case (3), k ends up in the hsq_kvs (soon to be renamed to hsq_implicit) field of the HsQTyVars for D1. After kind inference, I've written a check to make sure k appears free in the kind of a tyvar. That works. The problem is that the check also snags cases (1) and (2): my check uses the name from the LHsQTyVars, and with SigTvs in the mix, (1) and (2) end up with kind variables with names different from the names in the LHsQTyVars.
> 
> I'm sure there's some way to disentangle all of this, but I've given it a rest for now. This hit me in the fact that performance test case T9872d is like case (1), and the SigTvs threw my check off. But removing it caused problems elsewhere.
> 
> I'd enjoy discussing next week.
> 
> Thanks,
> Richard
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs