GHC infers over-polymorphic kinds

Consider

data T ka (a::ka) b  = MkT (T Type           Int   Bool)
                           (T (Type -> Type) Maybe Bool)

GHC accepts this even though it uses polymorphic recursion. But it shouldn't -- we simply do not have reliable way to infer most general types in the presence of polymorphic recursion.

In more detail, in getInitialKinds, GHC chooses this (bogus) "monomorphic" kind for T:

   T :: forall (ka :: kappa1) -> ka -> kappa2 -> Type

where kappa1 and kappa1 are unification variables. Then it kind-checks the data constructor declaration, given this mono-kind -- and succeeds!

But this is extremely fragile. At call-sites of T we are going to instantiate T's kind. But what if kappa2 is (somewhere, somehow) late unified wtih ka. Then, when instantiating T's kind with ka := blahwe should get blah -> blha -> Type. So how it instantiates will vary depending on what we konw about kappa2.

No no no. The initial monomorphic kind of T (returned by getInitialKinds, and used when checking the recursive RHSs) should be

   T :: kappa1 -> kappa2 -> kappa3 -> Type

Then indeed this program will be rejected, but so be it.

changed weight to 5

added Tbug Trac import labels

mentioned in issue #16347 (closed)

changed the description

Simon has proposed a fix:

In TcHsType, we find this, under kcLHsQTyVars_NonCusk:

    mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
    -- See Note [Dependent LHsQTyVars]
    mk_tc_binder hs_tv tv
       | hsLTyVarName hs_tv `elemNameSet` dep_names
       = mkNamedTyConBinder Required tv
       | otherwise
       = mkAnonTyConBinder tv

Simon suggests that changing it to this fixes the bug:

    mk_tc_binder :: LHsTyVarBndr GhcRn -> TyVar -> TyConBinder
    mk_tc_binder hs_tv tv
       = mkAnonTyConBinder tv

Note: just deleting code!

Indeed, this change fixes the example in the ticket because it effectively forgets that the first argument to T and the kind of the second are related. The program above is rejected right in the kc pass, because GHC tries to unify ka (a TyVarTv) with Type when looking at Int (never mind the Maybe it will see soon). Some examples are rejected in the tc pass though, like this:

data T2 ka (a::ka) = MkT2 (T2 Type a)

All fine during kc, but then once we produce T2 :: forall ka -> ka -> Type, failure in tc. While I'm never comfortable with non-CUSK types being rejected in the tc pass, I suppose it's OK.

More problematically, this is never rejected at all:

data T3 ka (a::ka) = forall b. MkT3 (T3 Type b)

This is accepted outright. The kc pass assigns kind ka to b (fine) and then the tc pass instantiates ka to be Type and assigns kind Type to b. Also fine (it's type-correct), but T3 is polymorphically recursive, and should be rejected.

So, I claim that Simon's fix makes these examples (erroneously accepted polymorphic recursion) harder to find, but doesn't get rid of them all. Instead, a more involved fix would be to, for example, require that all of these types are immediately followed by ka at recursive occurrences -- anything other than a first argument of ka is rejected. I'm not sure how to achieve this elegantly (haven't thought about it), but that should stamp out the problem.

Branch wip/over-poly-kinds, MR 436

Fixed in 1f5cc9dc.

closed

changed milestone to %8.10.1

marked this issue as related to #16347 (closed)

Test cases

• typecheck/should_compile/T16344b
• typecheck/should_fail/T16344
• typecheck/should_fail/T16344a

added Pnormal label

mentioned in commit b4f9ed63

changed the description

mentioned in merge request !9480 (merged)

mentioned in issue #22560 (closed)