Opened 19 months ago
Last modified 16 months ago
#14877 new bug
QuantifiedConstraints: Can't deduce `xx' from `(xx => a, xx)'
Reported by: | Iceland_jack | Owned by: | |
---|---|---|---|
Priority: | normal | Milestone: | |
Component: | Compiler | Version: | 8.5 |
Keywords: | QuantifiedConstraints | Cc: | |
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
This works with the latest change to the -XQuantifiedConstraints branch.
{-# Language QuantifiedConstraints, FlexibleInstances, MultiParamTypeClasses, AllowAmbiguousTypes, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances #-} class (forall xx. (xx => a) => Implies xx b) => F a b instance (forall xx. (xx => a) => Implies xx b) => F a b class (a => b) => Implies a b instance (a => b) => Implies a b
but replacing Implies xx b
with (xx => b)
causes it to fail. I don't know if the cause of this overlaps with an existing ticket.
class (forall xx. (xx => a) => (xx => b)) => F a b instance (forall xx. (xx => a) => (xx => b)) => F a b -- $ ghci -ignore-dot-ghci /tmp/ASD.hs -- GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help -- [1 of 1] Compiling Main ( /tmp/ASD.hs, interpreted ) -- -- /tmp/ASD.hs:4:10: error: -- • Could not deduce: xx0 -- arising from the superclasses of an instance declaration -- from the context: forall (xx :: Constraint). (xx => a, xx) => b -- bound by the instance declaration at /tmp/ASD.hs:4:10-53 -- or from: (xx => a, xx) -- bound by a quantified context at /tmp/ASD.hs:1:1 -- • In the instance declaration for ‘F a b’ -- | -- 4 | instance (forall xx. (xx => a) => (xx => b)) => F a b -- | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ -- Failed, no modules loaded. -- Prelude>
Change History (3)
comment:1 Changed 19 months ago by
Version: | 8.2.2 → 8.5 |
---|
comment:2 Changed 19 months ago by
comment:3 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
Note: See
TracTickets for help on using
tickets.
Consider the quantified constraint (QC) in
It serves as a local instance declaration. To construct the dictionary for
(F a b)
I may need to to solve a constraint(Implies xx b)
. The QC says "if you want to solveImplies xx b
, then it suffices to provexx => a
". And to provexx => a
, the built-in rules assumexx
and try to provea
.It's quite different to say
That is precisely equivalant to
Now the QC says "if you want to solve the goal
b
, then conjure up some constraintxx
, and prove(xx => a, xx)
. But how can we guessxx
?Each QC has an instance "head", usually headed by a type constructor, sometimes by a type variable. That head is the pattern the QC can solve.
Implies xx b
is a good instance head: it matches things of that form. Plainb
is not a good instance head!In short, I see nothing wrong here.