[GHC] #16344: GHC infers over-polymorphic kinds

[GHC]

#16344: GHC infers over-polymorphic kinds
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.6.3
      Resolution:                    |             Keywords:
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:

> 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) -> ak -> 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 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.

New description:

 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 := blah`we 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.

--

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16344#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler