decideKindGeneralisationPlan is too complicated
Consider this program, which originally comes from #14846 (closed). 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)’