#7862 closed bug (fixed)
Could not deduce (A) from the context (A, ...)
Reported by: | alang9 | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler (Type checker) | Version: | 7.8.3 |
Keywords: | Cc: | hackage.haskell.org@… | |
Operating System: | Linux | Architecture: | x86_64 (amd64) |
Type of failure: | GHC rejects valid program | Test Case: | indexed-types/should_compile/T7862 |
Blocked By: | Blocking: | ||
Related Tickets: | Differential Rev(s): | ||
Wiki Page: |
Description
The following code doesn't compile and produces a strange error:
{-# LANGUAGE TypeFamilies, FlexibleContexts #-} module Numeric.AD.Internal.Tower () where type family Scalar t newtype Tower s a = Tower [a] type instance Scalar (Tower s a) = a class (Num (Scalar t), Num t) => Mode t where (<+>) :: t -> t -> t instance (Num a) => Mode (Tower s a) where Tower as <+> _ = undefined where _ = (Tower as) <+> (Tower as) instance Num a => Num (Tower s a) where
src/Numeric/AD/Internal/Tower.hs:17:24: Could not deduce (Num (Scalar (Tower s a))) arising from a use of `<+>' from the context (Num (Scalar (Tower s a)), Num (Tower s a), Num a) bound by the instance declaration at src/Numeric/AD/Internal/Tower.hs:14:10-36 Possible fix: add an instance declaration for (Num (Scalar (Tower s a))) In the expression: (Tower as) <+> (Tower as) In a pattern binding: _ = (Tower as) <+> (Tower as) In an equation for `<+>': (Tower as) <+> _ = undefined where _ = (Tower as) <+> (Tower as)
Furthermore, Removing the Num (Scalar t)
constraint from the Mode
class produces a different strange error:
src/Numeric/AD/Internal/Tower.hs:17:24: Overlapping instances for Num (Tower s0 a) arising from a use of `<+>' Matching givens (or their superclasses): (Num (Tower s a)) bound by the instance declaration at src/Numeric/AD/Internal/Tower.hs:14:10-36 Matching instances: instance Num a => Num (Tower s a) -- Defined at src/Numeric/AD/Internal/Tower.hs:19:10 (The choice depends on the instantiation of `a, s0') In the expression: (Tower as) <+> (Tower as) In a pattern binding: _ = (Tower as) <+> (Tower as) In an equation for `<+>': (Tower as) <+> _ = undefined where _ = (Tower as) <+> (Tower as)
Change History (11)
comment:1 Changed 5 years ago by
Cc: | hackage.haskell.org@… added |
---|
comment:2 Changed 5 years ago by
difficulty: | → Unknown |
---|
comment:3 Changed 5 years ago by
commit db07129cfb13a856f31276c76e9e00924835b18e Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Thu May 2 17:14:23 2013 +0100 Eliminate (given) flatten-skolems in favour of user type variables See Note [Eliminate flat-skols]. IT wasn't exactly wrong before the the error messages are deeply strange.
comment:4 Changed 5 years ago by
OK, so now we get (from the original program)
T7862a.hs:17:24: Overlapping instances for Num (Tower s0 a) arising from a use of ‛<+>’ Matching givens (or their superclasses): (Num (Tower s a)) bound by the instance declaration at T7862a.hs:14:10-36 Matching instances: instance Num a => Num (Tower s a) -- Defined at T7862a.hs:19:10 (The choice depends on the instantiation of ‛a, s0’) In the expression: (Tower as) <+> (Tower as)
which is better but not good. For two reasons:
- The "matching given" comes from one of the "silent supperclass" parameters, which is confusing to the user.
- The whole thing is really due to the ambiguity of
s0
, and that's not even reported.
The reason we are careful about overlap between givens and instances is desribed in Note [Instance and Given overlap]
in TcInteract
.
I'm not sure what to do here. I'm expecting it's not a show-stopper for you: just add a type signature to resolve the ambiguity.
comment:5 Changed 3 years ago by
Another example of this bug:
{-# LANGUAGE AllowAmbiguousTypes, DefaultSignatures, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, UndecidableInstances, PolyKinds, ConstraintKinds, InstanceSigs, TypeFamilies #-} module Control.SmallCategory where import GHC.Exts import Control.Category class Vacuous (a:: i) instance Vacuous a class SmallCategory cat where type Objects cat :: i -> Constraint type Objects cat = Vacuous type Morphisms cat :: a -> a -> b id :: (Objects cat a) => (Morphisms cat) a a (.) :: (Objects cat a, Objects cat b, Objects cat c) => (Morphisms cat) b c -> (Morphisms cat) a b -> (Morphisms cat) a c instance (Category c, Category (Morphisms c)) => SmallCategory c where type Objects c = Vacuous type (Morphisms c) = c id = Control.Category.id (.) = (Control.Category..) src/Control/SmallCategory.hs:34:10: Could not deduce (Category (Morphisms c)) arising from a use of ‘Control.Category.id’ from the context (Category c, Category (Morphisms c)) bound by the instance declaration at src/Control/SmallCategory.hs:31:10-64 or from (Objects c a) bound by the type signature for id :: (Objects c a) => Morphisms c a a at src/Control/SmallCategory.hs:34:5-6 In the expression: Control.Category.id In an equation for ‘id’: id = Control.Category.id In the instance declaration for ‘SmallCategory c’ src/Control/SmallCategory.hs:35:11: Could not deduce (Category (Morphisms c)) arising from a use of ‘Control.Category..’ from the context (Category c, Category (Morphisms c)) bound by the instance declaration at src/Control/SmallCategory.hs:31:10-64 or from (Objects c a, Objects c b, Objects c c1) bound by the type signature for (.) :: (Objects c a, Objects c b, Objects c c1) => Morphisms c b c1 -> Morphisms c a b -> Morphisms c a c1 at src/Control/SmallCategory.hs:35:5-7 In the expression: (Control.Category..) In an equation for ‘.’: (.) = (Control.Category..) In the instance declaration for ‘SmallCategory c’
in 7.8.3.
comment:6 Changed 3 years ago by
Version: | 7.6.2 → 7.8.3 |
---|
comment:7 Changed 3 years ago by
The problem in comment:5 is unrelated to the original bug report -- it is a PolyKinds issue. If you turn on -fprint-explicit-kinds
, you get
Could not deduce (Category k2 (Morphisms (k -> k -> *) k2 * c)) arising from a use of ‘Control.Category.id’ from the context (Category k c, Category k1 (Morphisms (k -> k -> *) k1 * c)) bound by the instance declaration at Scratch.hs:30:10-64 or from (Objects (k -> k -> *) k2 c a) bound by the type signature for id :: (Objects (k -> k -> *) k2 c a) => Morphisms (k -> k -> *) k2 * c a a at Scratch.hs:33:5-6 In the expression: Control.Category.id In an equation for ‘id’: id = Control.Category.id In the instance declaration for ‘SmallCategory (k -> k -> *) c’
and you can see a more sensible error message.
What would be nice here is a note suggesting to turn on -fprint-explicit-kinds
.
comment:8 Changed 3 years ago by
Test Case: | → indexed-types/should_compile/T7862 |
---|
comment:10 Changed 23 months ago by
Milestone: | → 8.0.1 |
---|---|
Resolution: | → fixed |
Status: | new → closed |
This was fixed in commit a6f0f5ab45b2643b561e0a0a54a4f14745ab2152:
Author: Simon Peyton Jones <simonpj@microsoft.com> Date: Tue Dec 23 15:39:50 2014 +0000 Eliminate so-called "silent superclass parameters" The purpose of silent superclass parameters was to solve the awkward problem of superclass dictinaries being bound to bottom. See THE PROBLEM in Note [Recursive superclasses] in TcInstDcls Although the silent-superclass idea worked, * It had non-local consequences, and had effects even in Haddock, where we had to discard silent parameters before displaying instance declarations * It had unexpected peformance costs, shown up by Trac #3064 and its test case. In monad-transformer code, when constructing a Monad dictionary you had to pass an Applicative dictionary; and to construct that you neede a Functor dictionary. Yet these extra dictionaries were often never used. (All this got much worse when we added Applicative as a superclass of Monad.) Test T3064 compiled *far* faster after silent superclasses were eliminated. * It introduced new bugs. For example SilentParametersOverlapping, T5051, and T7862, all failed to compile because of instance overlap directly because of the silent-superclass trick. So this patch takes a new approach, which I worked out with Dimitrios in the closing hours before Christmas. It is described in detail in THE PROBLEM in Note [Recursive superclasses] in TcInstDcls. Seems to work great! Quite a bit of knock-on effect * The main implementation work is in tcSuperClasses in TcInstDcls Everything else is fall-out * IdInfo.DFunId no longer needs its n-silent argument * Ditto IDFunId in IfaceSyn * Hence interface file format changes * Now that DFunIds do not have silent superclass parameters, printing out instance declarations is simpler. There is tiny knock-on effect in Haddock, so that submodule is updated * I realised that when computing the "size of a dictionary type" in TcValidity.sizePred, we should be rather conservative about type functions, which can arbitrarily increase the size of a type. Hence the new datatype TypeSize, which has a TSBig constructor for "arbitrarily big". * instDFunType moves from TcSMonad to Inst * Interestingly, CmmNode and CmmExpr both now need a non-silent (Ord r) in a couple of instance declarations. These were previously silent but must now be explicit. * Quite a bit of wibbling in error messages
The test output is now:
T7862.hs:23:10: Warning: No explicit implementation for ‘+’, ‘*’, ‘abs’, ‘signum’, ‘fromInteger’, and (either ‘negate’ or ‘-’) In the instance declaration for ‘Num (Tower s a)’
comment:11 Changed 23 months ago by
Milestone: | 8.0.1 |
---|
The error is indeed strange. With a minor variant I got
Whoa! Look at that alternation of
Tower
andScalar
! Nothing like that shows up in the program.Turned out that it was to do with flattening type-function applications. After all, taking the strange constraint above, we see:
by using the
type instance
twice... and that is a much more sensible constraint. Turned out that the constraint solver was mis-orienting an equality so that, in effect, it reported a much less perspicuous (albeit still equivalent) version of constraint.