Skip to content

GitLab

GHC
GHC
Closed
Opened by Simon Peyton Jones@simonpjDeveloper

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. 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 decides this "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 := blah we might get blah -> blah -> Type or blah -> kappa2 -> Type, depending on whether kappa2 := ka has happened yet.

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.

Edited by Simon Peyton Jones