#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

#15141: decideKindGeneralisationPlan is too complicated -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: 8.8.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): Phab:D4971 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg <rae@…>): In [changeset:"c955a514f033a12f6d0ab0fbacec3e18a5757ab5/ghc" c955a51/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="c955a514f033a12f6d0ab0fbacec3e18a5757ab5" Remove decideKindGeneralisationPlan TypeInType came with a new function: decideKindGeneralisationPlan. This type-level counterpart to the term-level decideGeneralisationPlan chose whether or not a kind should be generalized. The thinking was that if `let` should not be generalized, then kinds shouldn't either (under the same circumstances around -XMonoLocalBinds). However, this is too conservative -- the situation described in the motivation for "let should be be generalized" does not occur in types. This commit thus removes decideKindGeneralisationPlan, always generalizing. One consequence is that tc_hs_sig_type_and_gen no longer calls solveEqualities, which reports all unsolved constraints, instead relying on the solveLocalEqualities in tcImplicitTKBndrs. An effect of this is that reporing kind errors gets delayed more frequently. This seems to be a net benefit in error reporting; often, alongside a kind error, the type error is now reported (and users might find type errors easier to understand). Some of these errors ended up at the top level, where it was discovered that the GlobalRdrEnv containing the definitions in the local module was not in the TcGblEnv, and thus errors were reported with qualified names unnecessarily. This commit rejiggers some of the logic around captureTopConstraints accordingly. One error message (typecheck/should_fail/T1633) is a regression, mentioning the name of a default method. However, that problem is already reported as #10087, its solution is far from clear, and so I'm not addressing it here. This commit fixes #15141. As it's an internal refactor, there is no concrete test case for it. Along the way, we no longer need the hsib_closed field of HsImplicitBndrs (it was used only in decideKindGeneralisationPlan) and so it's been removed, simplifying the datatype structure. Along the way, I removed code in the validity checker that looks at coercions. This isn't related to this patch, really (though it was, at one point), but it's an improvement, so I kept it. This updates the haddock submodule. }}} -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15141#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler