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 <[email protected]> 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 > [email protected] > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs _______________________________________________ ghc-devs mailing list [email protected] http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
