[GHC] #14010: UndecidableSuperClasses - Could not deduce (Category d)

#14010: UndecidableSuperClasses - Could not deduce (Category d) -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Keywords: | Operating System: Unknown/Multiple UndecidableSuperClasses | Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- Consider this well-typed code: {{{#!hs {-# LANGUAGE NoImplicitPrelude, TypeInType, TypeFamilies, UndecidableSuperClasses, RankNTypes, TypeOperators, FlexibleContexts, TypeSynonymInstances, FlexibleInstances, UndecidableInstances #-} module Monolith where import Data.Kind (Type) import GHC.Exts (Constraint) type family (~>) :: c -> c -> Type type instance (~>) = (->) type instance (~>) = ArrPair type family Fst (p :: (a, b)) :: a where Fst '(x, _) = x type family Snd (p :: (a, b)) :: b where Snd '(_, y) = y data ArrPair a b = ArrPair (Fst a ~> Fst b) (Snd a ~> Snd b) type family Super c :: Constraint where Super Type = () Super (c, d) = (Category c, Category d) class Super cat => Category cat where id :: forall (a :: cat). a ~> a instance Category Type where id = \x -> x instance (Category c, Category d) => Category (c, d) where id = ArrPair id id class Category (c, d) => Functor (f :: c -> d) where --class (Category c, Category d) => Functor (f :: c -> d) where map :: (a ~> b) -> (f a ~> f b) data OnSnd f a b = OnSnd (f '(a, b)) instance Functor (f :: (c, d) -> Type) => Functor (OnSnd f a) where map f (OnSnd x) = OnSnd (map (ArrPair id f) x) }}} The compiler accepts it. But if I change the definition of 'Functor' for the commented one, I get an error: {{{ super.hs:39:10: error: • Could not deduce (Category d) arising from the superclasses of an instance declaration from the context: Functor f bound by the instance declaration at super.hs:39:10-61 Possible fix: add (Category d) to the context of the instance declaration • In the instance declaration for ‘Functor (OnSnd f a)’ | 39 | instance Functor (f :: (c, d) -> Type) => Functor (OnSnd f a) where | }}} I can reproduce this on 8.0.1, 8.2.0.20170704 and HEAD. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14010 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14010: UndecidableSuperClasses - Could not deduce (Category d) -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by Iceland_jack): * cc: Iceland_jack (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14010#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14010: UndecidableSuperClasses - Could not deduce (Category d) -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): GHC's error message looks absolutely right to me. Writing in the kinds we have {{{ Functor :: forall c d. (c -> d) -> Constraint OnSnd :: forall c d. ((c,d) -> *) -> c -> d -> * class (Category c, Category d) => MyFunctor @c @d (f :: c -> d) where instance MyFunctor @(c,d) @* (f2 :: (c, d) -> *) => MyFunctor @d @* (OnSnd @c @d f2 (a::c)) where }}} From the instance declaration we are obliged to generate superclasses for `MyFunctor @d @* (OnSnd @c @d f2 (a::c))`, namely {{{ [W] Category d [W] Category * }}} The latter is no problem, but `Category d` is. What do we have available to prove it? Just the instance context {{{ [G] MyFunctor @(c,d) @* (f2 :: (c,d) -> *) }}} If we have that given, then we have its superclasses given: {{{ [G] Category (c,d) [G] Category * }}} Can we prove `Category d` given `Category (c,d)`? No we cannot. And that is just what GHC says. Here it is with `-fprint-explicit-kinds`: {{{ T14010.hs:45:10: error: * Could not deduce (Category d) arising from the superclasses of an instance declaration from the context: MyFunctor (c, d) * f2 bound by the instance declaration at T14010.hs:(45,10)-(46,31) }}} So I claim this is a non-bug. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14010#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14010: UndecidableSuperClasses - Could not deduce (Category d) -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index):
Can we prove Category d given Category (c,d)? No we cannot.
Yes, we can. The declaration of `Category` is `Super cat => Category cat`, so from `Category (c, d)` we can prove `Super (c, d)`, which reduces to `(Category c, Category d)`. Furthermore, if you study the original code that compiles, you can see that GHC manages to go via a similar route just fine. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14010#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14010: UndecidableSuperClasses - Could not deduce (Category d) -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index): To clarify, you say that given {{{ [G] Functor @(c,d) @* (f2 :: (c,d) -> *) }}} we have its superclasses: {{{ [G] Category (c,d) [G] Category * }}} and you claim we can't prove `[W] Category d` from this. But with the definition of `Functor` that does compile, the superclasses are: {{{ [G] Category ((c,d), *) }}} and GHC will want to extract `[W] Category (d, *)` from it. So GHC appears to do more work here! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14010#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14010: UndecidableSuperClasses - Could not deduce (Category d) -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: | UndecidableSuperClasses Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Ah yes, you are right. It took me some time to recall. It's all described in this note, in `TcInstDcls`. {{{ Note [Recursive superclasses] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ See Trac #3731, #4809, #5751, #5913, #6117, #6161, which all describe somewhat more complicated situations, but ones encountered in practice. See also tests tcrun020, tcrun021, tcrun033, and Trac #11427. ----- THE PROBLEM -------- The problem is that it is all too easy to create a class whose superclass is bottom when it should not be. Consider the following (extreme) situation: class C a => D a where ... instance D [a] => D [a] where ... (dfunD) instance C [a] => C [a] where ... (dfunC) Although this looks wrong (assume D [a] to prove D [a]), it is only a more extreme case of what happens with recursive dictionaries, and it can, just about, make sense because the methods do some work before recursing. To implement the dfunD we must generate code for the superclass C [a], which we had better not get by superclass selection from the supplied argument: dfunD :: forall a. D [a] -> D [a] dfunD = \d::D [a] -> MkD (scsel d) .. Otherwise if we later encounter a situation where we have a [Wanted] dw::D [a] we might solve it thus: dw := dfunD dw Which is all fine except that now ** the superclass C is bottom **! The instance we want is: dfunD :: forall a. D [a] -> D [a] dfunD = \d::D [a] -> MkD (dfunC (scsel d)) ... ----- THE SOLUTION -------- The basic solution is simple: be very careful about using superclass selection to generate a superclass witness in a dictionary function definition. More precisely: Superclass Invariant: in every class dictionary, every superclass dictionary field is non-bottom To achieve the Superclass Invariant, in a dfun definition we can generate a guaranteed-non-bottom superclass witness from: (sc1) one of the dictionary arguments itself (all non-bottom) (sc2) an immediate superclass of a smaller dictionary (sc3) a call of a dfun (always returns a dictionary constructor) The tricky case is (sc2). We proceed by induction on the size of the (type of) the dictionary, defined by TcValidity.sizeTypes. Let's suppose we are building a dictionary of size 3, and suppose the Superclass Invariant holds of smaller dictionaries. Then if we have a smaller dictionary, its immediate superclasses will be non-bottom by induction. What does "we have a smaller dictionary" mean? It might be one of the arguments of the instance, or one of its superclasses. Here is an example, taken from CmmExpr: class Ord r => UserOfRegs r a where ... (i1) instance UserOfRegs r a => UserOfRegs r (Maybe a) where (i2) instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where For (i1) we can get the (Ord r) superclass by selection from (UserOfRegs r a), since it is smaller than the thing we are building (UserOfRegs r (Maybe a). But for (i2) that isn't the case, so we must add an explicit, and perhaps surprising, (Ord r) argument to the instance declaration. Here's another example from Trac #6161: class Super a => Duper a where ... class Duper (Fam a) => Foo a where ... (i3) instance Foo a => Duper (Fam a) where ... (i4) instance Foo Float where ... It would be horribly wrong to define dfDuperFam :: Foo a -> Duper (Fam a) -- from (i3) dfDuperFam d = MkDuper (sc_sel1 (sc_sel2 d)) ... dfFooFloat :: Foo Float -- from (i4) dfFooFloat = MkFoo (dfDuperFam dfFooFloat) ... Now the Super superclass of Duper is definitely bottom! This won't happen because when processing (i3) we can use the superclasses of (Foo a), which is smaller, namely Duper (Fam a). But that is *not* smaller than the target so we can't take *its* superclasses. As a result the program is rightly rejected, unless you add (Super (Fam a)) to the context of (i3). Note [Solving superclass constraints] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ How do we ensure that every superclass witness is generated by one of (sc1) (sc2) or (sc3) in Note [Recursive superclasses]. Answer: * Superclass "wanted" constraints have CtOrigin of (ScOrigin size) where 'size' is the size of the instance declaration. e.g. class C a => D a where... instance blah => D [a] where ... The wanted superclass constraint for C [a] has origin ScOrigin size, where size = size( D [a] ). * (sc1) When we rewrite such a wanted constraint, it retains its origin. But if we apply an instance declaration, we can set the origin to (ScOrigin infinity), thus lifting any restrictions by making prohibitedSuperClassSolve return False. * (sc2) ScOrigin wanted constraints can't be solved from a superclass selection, except at a smaller type. This test is implemented by TcInteract.prohibitedSuperClassSolve * The "given" constraints of an instance decl have CtOrigin GivenOrigin InstSkol. * When we make a superclass selection from InstSkol we use a SkolemInfo of (InstSC size), where 'size' is the size of the constraint whose superclass we are taking. An similarly when taking the superclass of an InstSC. This is implemented in TcCanonical.newSCWorkFromFlavored }}} In this case we have {{{ We are making superclasses of: [W] Functor @d @* (OnSnd c d f2 a) Can we use superclasses of this? [G] Functor @((,) * * c d) @* f2 }}} The and the number of syntax nodes [G] is not smaller than that of [W], so we say "No". The relevant function is `TcSMonad.prohibitedSuperClassSolve`. We could perhaps "fix" this example by changing the size metric used for types. But then perhaps something else would go wrong. There is a workaround, as you observe. I wish I knew a better way. But, believe me, the convolutions to avoid generation superclasses that were accidentally bottom were MUCH worse before. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14010#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC