[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
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 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.

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