Opened 18 months ago

Last modified 16 months ago

#14958 new bug

QuantifiedConstraints: Doesn't apply implication for existential?

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 fails

{-# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes #-}

data Foo where
  Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo

a :: Foo
a = Foo 10
$ ... -ignore-dot-ghci /tmp/Optic.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/Optic.hs, interpreted )

/tmp/Optic.hs:7:9: error:
    • Could not deduce (Num x) arising from the literal ‘10’
      from the context: (forall y. cls0 y => Num y, cls0 x)
        bound by a type expected by the context:
                   forall x. (forall y. cls0 y => Num y, cls0 x) => x
        at /tmp/Optic.hs:7:5-10
      Possible fix:
        add (Num x) to the context of
          a type expected by the context:
            forall x. (forall y. cls0 y => Num y, cls0 x) => x
    • In the first argument of ‘Foo’, namely ‘10’
      In the expression: Foo 10
      In an equation for ‘a’: a = Foo 10
  |
7 | a = Foo 10
  |         ^^
Failed, no modules loaded.
Prelude> 

GHC knows that cls ~=> Num but still GHC cannot deduce Num x from cls x.


The reason for trying this is creating a newtype for optics where we still get subsumption

{-# Language GADTs, RankNTypes, ConstraintKinds, QuantifiedConstraints, AllowAmbiguousTypes, ApplicativeDo, TypeOperators, MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, PolyKinds, FlexibleContexts #-}

data Optic cls s a where
  Optic :: (forall f. cls f => (a -> f a) -> (s -> f s)) -> Optic cls s a

class    (forall x. f x => g x) => (f ~=> g)
instance (forall x. f x => g x) => (f ~=> g)

_1 :: cls ~=> Functor => Optic cls (a, b) a
_1 = Optic $ \f (a, b) -> do
  a' <- f a
  pure (a', b)

lens_1 :: Optic Functor (a, b) a
lens_1 = _1

trav_1 :: Optic Applicative (a, b) a
trav_1 = _1

and I wanted to move cls ~=> Functor into the Optic type itself.

Change History (6)

comment:1 Changed 18 months ago by simonpj

This is to do with overlapping instances. We have

  Foo :: (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo

So from the expression Foo 10 we have: Given:

  Skolems: x
  Given:  d1: forall y. cls0 y => Num y
          d2: cls0 x

  Wanted: Num x

Here cls0 is a unification variable; we don't yet know what it'll tur out to be, and indeed (given the type of Foo) it's ambiguous.

When trying to solve Num x GHC doesn't want to use d1, because that make a commitment to solve its sub-goals. If cls0 turned out to be Num, an alternative would be to pick d2. So it simply refrains from choosing. (The error message doesn't make this clear, I know.)

If you fix cls0 all is well. For example:

data Foo (cls :: * -> Constraint) where
  Foo :: forall cls.
           (forall x. ((forall y. cls y => Num y), cls x) => x)
           -> Foo cls

a :: Foo Fractional
a = Foo 10

comment:2 Changed 18 months ago by Iceland_jack

Ah! That makes perfect sense, we can specify a Proxy cls and not change the kind of Foo

data Foo where
  Foo :: Proxy cls -> (forall x. ((forall y. cls y => Num y), cls x) => x) -> Foo

a :: Foo
a = Foo (Proxy :: Proxy Num) 10

b :: Foo
b = Foo (Proxy :: Proxy Fractional) 10.0

(it's maybe not as clear as I thought: is it possible to convert Foo to data Foo2 = Foo2 (forall x. Num x => x)?)

I have a draft ready for an overview of this extension from ticket:14840#comment:6, should I email it to you?

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

comment:3 Changed 18 months ago by simonpj

I have a draft ready for an overview of this extension from ticket:14840#comment:6, should I email it to you?

A draft of what? A blog post? If so, I suggest you just post it!

comment:4 Changed 18 months ago by Iceland_jack

Ah I started writing it as a paper

comment:5 Changed 18 months ago by simonpj

Even better!

comment:6 Changed 16 months ago by RyanGlScott

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