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 Iceland_jack

The same happens if we add

instance (Refl rel, forall xx. xx) => Category (With rel) where

comment:2 Changed 19 months ago by simonpj

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 Iceland_jack

Summary: QuantifiedConstraints: Strengthening context causes failureQuantifiedConstraints: Adding to the context causes failure

comment:4 in reply to:  2 Changed 19 months ago by Iceland_jack

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
Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:5 Changed 19 months ago by RyanGlScott

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 Changed 19 months ago by simonpj

What is "this program"? The one in comment:4 uses CCategory but does not define it.

comment:7 Changed 19 months ago by RyanGlScott

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 in reply to:  6 Changed 19 months ago by Iceland_jack

Replying to simonpj:

What is "this program"? The one in comment:4 uses CCategory but does not define it.

ConstraintCategory was meant to be CCategory, I changed it to reflect that

comment:9 in reply to:  7 Changed 19 months ago by Iceland_jack

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 simonpj

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 Iceland_jack

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)
Last edited 19 months ago by Iceland_jack (previous) (diff)

comment:12 Changed 19 months ago by simonpj

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 in reply to:  12 Changed 19 months ago by Iceland_jack

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

  1. Dom / Cod are type families (#14860)
  2. We can't convert from a :- b to Dict (a => b) (#14822)
  3. Ignoring 1. / 2. for now, how can we even use ob to witness MapOb 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 simonpj

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:15 Changed 18 months ago by Iceland_jack

Solved here: gist

Last edited 18 months ago by Iceland_jack (previous) (diff)

comment:16 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.