Opened 19 months ago
Last modified 16 months ago
#14832 new bug
QuantifiedConstraints: Adding to the context causes failure
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
With Simon's latest changes (ticket:14733#comment:9) this works:
{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-} import Control.Category import Data.Kind import Data.Coerce data With cls a b where With :: cls a b => With cls a b type Coercion = With Coercible type Refl rel = (forall xx. rel xx xx :: Constraint) type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint) instance Refl rel => Category (With rel) where id = With (.) = undefined
But strengthening the context with Trans rel
:
instance (Refl rel, Trans rel) => Category (With rel) where
causes it to fail
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help [1 of 1] Compiling Main ( J.hs, interpreted ) J.hs:15:10: error: • Could not deduce: rel xx zz from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 or from: (rel xx yy, rel yy zz) bound by a quantified context at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ J.hs:15:10: error: • Could not deduce: rel xx xx from the context: (Refl rel, Trans rel) bound by an instance declaration: forall k (rel :: k -> k -> Constraint). (Refl rel, Trans rel) => Category (With rel) at J.hs:15:10-53 • In the ambiguity check for an instance declaration To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Failed, no modules loaded. Prelude>
Change History (16)
comment:1 Changed 19 months ago by
comment:2 follow-up: 4 Changed 19 months ago by
GHC is very careful about picking instances. See http://downloads.haskell.org/~ghc/master/users-guide/glasgow_exts.html#overlapping-instances, esp the bit about "all instances that unify".
The constraint rel xx xx
matches both (Refl rel)
and (Trans rel)
; but the (head of) the former is an instance of the (head of) the latter so it should win. At least with overlapping instances on. (There's no way to add an OVERLAPPING pragama to an individual quantified constraint -- yet anyway.)
The constraint rel xx zz
could (if zz
was further instantiated) match(Refl rel)
, so GHC refains from picking it. IncoherentInstnaces
might help.
In short, right now I'm being very conservative about ambiguity. Once we pick the "wrong" path there is no way back -- GHC does no backtracking.
I'm inclined to park this one until we have the basics nailed.
comment:3 Changed 19 months ago by
Summary: | QuantifiedConstraints: Strengthening context causes failure → QuantifiedConstraints: Adding to the context causes failure |
---|
comment:4 Changed 19 months ago by
Replying to simonpj:
I'm inclined to park this one until we have the basics nailed.
That's fine, this isn't (doesn't seem to be) a show stopper.
In this case I can encode these properties as a type class ((:-)
-enriched categories)
type ConstraintCat ob = ob -> ob -> Constraint class CCategory (cat::ConstraintCat ob) where cid :: () :- cat a a comp :: (cat a b, cat b c) :- cat a c instance CCategory cat => Category (With cat) where id :: forall a. With cat a a id = case cid :: () :- cat a a of Dict -> With (.) :: forall b c a. With cat b c -> With cat a b -> With cat a c With . With = case ccomp :: (cat a b, cat b c) :- cat a c of Dict -> With
comment:5 Changed 19 months ago by
Using the latest commit on the wip/T2893
branch, this program now gives you a stack overflow!
$ inplace/bin/ghc-stage2 --interactive ../Bug.hs GHCi, version 8.5.20180128: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( ../Bug.hs, interpreted ) ../Bug.hs:15:10: error: • Reduction stack overflow; size = 201 When simplifying the following type: rel xx yy0 Use -freduction-depth=0 to disable this check (any upper bound you could choose might fail unpredictably with minor updates to GHC, so disabling the check is recommended if you're sure that type checking should terminate) • In the instance declaration for ‘Category (With rel)’ | 15 | instance (Refl rel, Trans rel) => Category (With rel) where | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
comment:6 follow-up: 8 Changed 19 months ago by
What is "this program"? The one in comment:4 uses CCategory
but does not define it.
comment:7 follow-up: 9 Changed 19 months ago by
I'm referring to the original program itself:
{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-} import Control.Category import Data.Kind import Data.Coerce data With cls a b where With :: cls a b => With cls a b type Coercion = With Coercible type Refl rel = (forall xx. rel xx xx :: Constraint) type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint) instance (Refl rel, Trans rel) => Category (With rel) where id = With (.) = undefined
comment:8 Changed 19 months ago by
comment:9 Changed 19 months ago by
Replying to RyanGlScott:
I'm referring to the original program itself:
The original program still gives a stack overflow with latest changes.
comment:10 Changed 19 months ago by
The original program still gives a stack overflow with latest changes.
And so it should. You have a "given" (Trans rel)
, where
{{
type Trans rel = (forall xx yy zz. (rel xx yy, rel yy zz) => rel xx zz :: Constraint)
}}}
So if you want to solve [W] rel t1 t2
(for some type t1
or t2
, this local instance (quantified constraint) matches. We can solve it by solving
[W] rel t1 alpha [W] rel alpha t2
where alpha
is a fresh unification variable (corresponding to yy
in the definition of Trans rel
.
But then each of those two constraints can be solved once more with this over-general local instance -- and now we hare four constraints. And so on. You used UndecidableInstances
and sure enough you wrote an infinite loop.
I say there is no bug here. The same thing wold happen if you wrote
instance (C a x, C x b) => C a b
comment:11 Changed 19 months ago by
Is there hope for the user to guide this process and leaving the definition of Trans
intact (not having to create CCategory
)?
If this were a rank-2 function we can explicitly instantiate xx
yy
zz
foo :: R X Y -> R Y Z -> (forall xx yy zz. (R xx yy, R yy zz) -> R xx zz) -> R X Y foo xy yz f = f @X @Y @Z (xy, yz)
comment:12 follow-up: 13 Changed 19 months ago by
Is there hope for the user to guide this process
You want to write a term-level function that can be used a theorem in solving type-level constraints. This also came up, I think, in #14822.
Of course, this is much what happens in many proof assistants. Perhaps we can learn from them. Personally, I don't see a direct way to do this; but perhaps others with a broader perspective, and a bit more time, might do so.
comment:13 Changed 19 months ago by
Replying to simonpj:
You want to write a term-level function that can be used a theorem in solving type-level constraints.
That's right.
Here are some thoughts I have on a meatier example I just ran into. Each category in hask
has an associated constraint for objects (Ob cat a
). If a
is an object of Dom f
and f
is a functor then f a
must be an object of Cod f
ob :: Functor f => Ob (Dom f) a :- Ob (Cod f) (f a) ob = Sub (source (fmap id))
Constructing this relies crucially on fmap
and friends at the term level.
The user has to pry ob
open (at the right type) (here they just wanted to write id = Nat id
)
id = Nat id1 where id1 :: forall f x. (Functor f, Ob (Dom f) x) => Cod f (f x) (f x) id1 = id \\ (ob :: Ob (Dom f) x :- Ob (Cod f) (f x))
It actually works today to add this implication to the superclass context of Functor f
but GHC will not use it and refuses to take our (term-level) ob
into account
type MapOb f = (forall x. Ob (Dom f) x => Ob (Cod f) (f x) :: Constraint) class (MapOb f, ..) => Functor f ..
I see several issues for what I just presented
Dom
/Cod
are type families (#14860)- We can't convert from
a :- b
toDict (a => b)
(#14822) - Ignoring 1. / 2. for now, how can we even use
ob
to witnessMapOb f
?
One idea is to allow pattern matching outside of case
expressions or indeed outside any definition, so we could write
reifyC :: (a :- b) -> Dict (a => b) reifyC = error "let's assume this for a second" class MapOb f => Functor f where -- This brings `MapOb f' into scope for the whole instance Dict <- reifyC (ob @_ @_ @f)
Am I off base here?
comment:14 Changed 18 months ago by
See also #14937. I'm too snowed under to think about this -- but open to worked-out suggestions if you want to progress it.
comment:16 Changed 16 months ago by
Keywords: | wipT2893 removed |
---|
The same happens if we add