#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