[GHC] #15141: decideKindGeneralisationPlan is too complicated

11 May 2018

      #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
           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 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.

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