Opened 2 years ago
Last modified 5 months ago
#7862 new bug
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 Revisions: |
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 (9)
comment:1 Changed 2 years ago by liyang
- Cc hackage.haskell.org@… added
comment:2 Changed 2 years ago by simonpj
- difficulty set to Unknown
comment:3 Changed 2 years ago by simonpj
commit db07129cfb13a856f31276c76e9e00924835b18e Author: Simon Peyton Jones <[email protected]> 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 2 years ago by simonpj
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 5 months ago by spacekitteh
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 5 months ago by spacekitteh
- Version changed from 7.6.2 to 7.8.3
comment:7 Changed 5 months ago by goldfire
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 5 months ago by simonpj
- Test Case set to indexed-types/should_compile/T7862
The error is indeed strange. With a minor variant I got
Whoa! Look at that alternation of Tower and Scalar! 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.