Opened 19 months ago

Closed 17 months ago

## #15141 closed bug (fixed)

# decideKindGeneralisationPlan is too complicated

Reported by: | simonpj | Owned by: | |
---|---|---|---|

Priority: | normal | Milestone: | 8.8.1 |

Component: | Compiler | Version: | 8.2.2 |

Keywords: | Cc: | ||

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: |

### Description (last modified by )

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)’

### Change History (5)

### comment:1 Changed 19 months ago by

Description: | modified (diff) |
---|

### comment:2 Changed 18 months ago by

Milestone: | 8.6.1 → 8.8.1 |
---|

### comment:3 Changed 17 months ago by

Differential Rev(s): | → Phab:D4971 |
---|---|

Status: | new → patch |

My solution to this is now on Phab. Awaiting review before committing.

**Note:**See TracTickets for help on using tickets.

These won't be addressed for GHC 8.6.