[GHC] #15141: decideKindGeneralisationPlan is too complicated

[GHC]

#15141: decideKindGeneralisationPlan is too complicated
-------------------------------------+-------------------------------------
        Reporter:  simonpj           |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:  8.6.1
       Component:  Compiler          |              Version:  8.2.2
      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 this program, which originally comes from #14846.  I have
> decorated it with kind signatures so you can see what is going on
> {{{
> {-# LANGUAGE AllowAmbiguousTypes #-}
> {-# LANGUAGE ConstraintKinds #-}
> {-# LANGUAGE EmptyCase #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE InstanceSigs #-}
> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE ScopedTypeVariables #-}
> {-# LANGUAGE TypeInType #-}
> module T14846 where
>
> import Data.Kind
> import Data.Proxy
>
> -- Cat :: * -> *
> type Cat ob = ob -> ob -> Type
>
> -- Struct :: forall k. (k -> Constraint) -> *
> data Struct :: (k -> Constraint) -> Type where
>   S :: Proxy (a::k) -> Struct (cls::k -> Constraint)
>
> -- Structured :: forall k
> --               forall (a:k) (cls:k->Constraint) -> Struct k cls
> type Structured a cls = (S ('Proxy :: Proxy a) :: Struct cls)
>
> -- AStruct :: forall k (cls : k->Constraint). Struct cls -> Type
> data AStruct :: Struct cls -> Type where
>   AStruct :: cls a => AStruct (Structured a cls)
>
> -- StructI :: forall k1 k2 (cls :: k2 -> Constraint).
> --            k1 -> Struct k2 cls -> Constraint
> class StructI xx (structured::Struct (cls :: k -> Constraint)) where
>   struct :: AStruct structured
>
> --  Hom :: forall k1 k2 (cls :: k2 -> Constraint).
> --         Cat k1 -> Cat (Struct {k2} cls)
> data Hom :: Cat k -> Cat (Struct cls) where
>
> -- Category :: forall ob. Cat ob -> Constraint
> class Category (cat::Cat ob) where
>   i :: StructI xx a => ríki a a
>
> instance forall (riki :: Cat kx)
>                 (cls  :: kk -> Constraint).
>          Category riki => Category (Hom riki :: Cat (Struct cls)) where
>   i :: forall xx a. StructI xx a => Hom riki a a
>   i = case struct :: AStruct (Structured a cls) of
> }}}
> Focus on the final instance declaration. Do kind inference on the type
> signature for `i`.
> I think we should get
> {{{
>   i :: forall {k1} {k2} {cls1 :: k2 -> Constraint}
>        forall (xx :: k1) (a :: Struct {k2} cls1).
>        StructI {k1} {k2} xx a => Hom {kx} {k2} riki a a
> }}}
> Nothing about `i`'s type signature constraints the `cls` to be the same
> as the
> in-scope `cls`.  Yes `riki` is in scope, but its kind is unrelated.
>
> But at present GHC does not kind-generalise `i`'s type (because of
> `kindGeneralisationPlan`),
> so random things in the body of `i` may influence how its kinds get
> fixed.   And if we changed
> the signature a bit so that it didn't mention `riki` any more, suddenly
> it ''would'' be kind-generalised.
>
> This seems incomprehensibly complicated to me.

New description:

 Consider this program, which originally comes from #14846.  I have
 decorated it with kind signatures so you can see what is going on
 {{{
 {-# LANGUAGE AllowAmbiguousTypes #-}
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE EmptyCase #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeInType #-}
 module T14846 where

 import Data.Kind
 import Data.Proxy

 -- Cat :: * -> *
 type Cat ob = ob -> ob -> Type

 -- Struct :: forall k. (k -> Constraint) -> *
 data Struct :: (k -> Constraint) -> Type where
   S :: Proxy (a::k) -> Struct (cls::k -> Constraint)

 -- Structured :: forall k
 --               forall (a:k) (cls:k->Constraint) -> Struct k cls
 type Structured a cls = (S ('Proxy :: Proxy a) :: Struct cls)

 -- AStruct :: forall k (cls : k->Constraint). Struct cls -> Type
 data AStruct :: Struct cls -> Type where
   AStruct :: cls a => AStruct (Structured a cls)

 -- StructI :: forall k1 k2 (cls :: k2 -> Constraint).
 --            k1 -> Struct k2 cls -> Constraint
 class StructI xx (structured::Struct (cls :: k -> Constraint)) where
   struct :: AStruct structured

 --  Hom :: forall k1 k2 (cls :: k2 -> Constraint).
 --         Cat k1 -> Cat (Struct {k2} cls)
 data Hom :: Cat k -> Cat (Struct cls) where

 -- Category :: forall ob. Cat ob -> Constraint
 class Category (cat::Cat ob) where
   i :: StructI xx a => ríki a a

 instance forall (riki :: Cat kx)
                 (cls  :: kk -> Constraint).
          Category riki => Category (Hom riki :: Cat (Struct cls)) where
   i :: forall xx a. StructI xx a => Hom riki a a
   i = case struct :: AStruct (Structured a cls) of
 }}}
 Focus on the final instance declaration. Do kind inference on the type
 signature for `i`.
 I think we should get
 {{{
   i :: forall {k1} {k2} {cls1 :: k2 -> Constraint}
        forall (xx :: k1) (a :: Struct {k2} cls1).
        StructI {k1} {k2} xx a => Hom {kx} {k2} riki a a
 }}}
 Nothing about `i`'s type signature constraints the `cls` to be the same as
 the
 in-scope `cls`.  Yes `riki` is in scope, but its kind is unrelated.

 But at present GHC does not kind-generalise `i`'s type (because of
 `kindGeneralisationPlan`),
 so random things in the body of `i` may influence how its kinds get fixed.
 And if we changed
 the signature a bit so that it didn't mention `riki` any more, suddenly
 it ''would'' be kind-generalised.

 This seems incomprehensibly complicated to me.

 Moreover, the type of `i` from the ''class'' decl:
 {{{
 class Category (cat::Cat ob) where
   i :: StructI xx a => ríki a a
 }}}
 comes out in its full glory as
 {{{
   i :: forall k1 k2 (cls :: k2 -> Constraint)
               (xx :: k1) (a :: Struct {k2} cls)
               (riki :: Cat (Struct {k2} cls).
        StructI {k1} {k2} cls xx a => riki a a
 }}}
 So indeed `i` is expected to be as polymorphic as I expected, and the
 unexpected
 lack of generalisation gives rise (in HEAD) to a bogus error:
 {{{
 T14846.hs:51:8: error:
     • Couldn't match type ‘ríki’ with ‘Hom kx k1 cls0 riki’
       ‘ríki’ is a rigid type variable bound by
         the type signature for:
           i :: forall k (cls1 :: k -> Constraint) k3 (xx :: k3) (a ::
 Struct
                                                                         k
 cls1) (ríki :: Struct
 k cls1
 -> Struct
 k cls1
 -> *).
                StructI k3 k cls1 xx a =>
                ríki a a
         at T14846.hs:51:8-51
       Expected type: ríki a a
         Actual type: Hom kx k1 cls0 riki a0 a0
     • When checking that instance signature for ‘i’
         is more general than its signature in the class
         Instance sig: forall (xx :: k0) (a :: Struct k1 cls0).
                       StructI k0 k1 cls0 xx a =>
                       Hom kx k1 cls0 riki a a
            Class sig: forall k1 (cls :: k1
                                         -> Constraint) k2 (xx :: k2) (a ::
 Struct
 k1 cls) (ríki :: Struct
 k1
 cls
 -> Struct
 k1
 cls
 -> *).
                       StructI k2 k1 cls xx a =>
                       ríki a a
       In the instance declaration for
         ‘Category {Struct kk cls} (Hom kx kk cls riki)’
 }}}

--

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