Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

#14863 closed bug (fixed)

QuantifiedConstraints: Can't deduce `c' from `(a, b)' and `a |- b |- c'

Reported by: Iceland_jack Owned by:
Priority: normal Milestone: 8.6.1
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: quantified-constraints/T14863
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

#14833 fixes #14835: we can witness curryC :: ((a, b) |- c) :- (a |- b |- c).

Now for the entirely predictable, how about uncurryC

{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs, LiberalTypeSynonyms, TypeOperators, MultiParamTypeClasses, FlexibleInstances #-}

data Dict c where
  Dict :: c => Dict c

infixr |-
class    (a => b) => (a |- b)
instance (a => b) => (a |- b)

type a :- b = Dict (a |- b)

uncurryC :: forall a b c. (a |- b |- c) :- ((a, b) |- c)
uncurryC = Dict
$ ghci -ignore-dot-ghci Z.hs 
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Z.hs, interpreted )

Z.hs:13:12: error:
    • Could not deduce: c arising from a use of ‘Dict’
      from the context: a |- (b |- c)
        bound by a quantified context at Z.hs:1:1
      or from: (a, b) bound by a quantified context at Z.hs:1:1
    • In the expression: Dict
      In an equation for ‘uncurryC’: uncurryC = Dict
    • Relevant bindings include
        uncurryC :: (a |- (b |- c)) :- ((a, b) |- c) (bound at Z.hs:13:1)
   |
13 | uncurryC = Dict
   |            ^^^^
Failed, no modules loaded.
Prelude> 

Change History (8)

comment:1 Changed 19 months ago by RyanGlScott

Once again, I think this :- thing is a red herring. Here's what I believe to be the essence of the bug:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
module Bug where

data Dict c where
  Dict :: c => Dict c

class    (a => b) => Implies a b
instance (a => b) => Implies a b

uncurryCImpredic1 :: forall a b c. Implies a (b => c) => Dict (Implies (a, b) c)
uncurryCImpredic1 = Dict

uncurryCImpredic2 :: forall a b c. a => Implies b c => Dict (Implies (a, b) c)
uncurryCImpredic2 = Dict

uncurryC1 :: forall a b c. (a => b => c) => Dict (Implies (a, b) c)
uncurryC1 = Dict

uncurryC2 :: forall a b c. Implies a (Implies b c) => Dict (Implies (a, b) c)
uncurryC2 = Dict
$ ghc-cq/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 Bug              ( Bug.hs, interpreted )

Bug.hs:27:13: error:
    • Could not deduce: c arising from a use of ‘Dict’
      from the context: Implies a (Implies b c)
        bound by the type signature for:
                   uncurryC2 :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                                Implies a (Implies b c) =>
                                Dict (Implies (a, b) c)
        at Bug.hs:26:1-77
      or from: (a, b) bound by a quantified context at Bug.hs:1:1
    • In the expression: Dict
      In an equation for ‘uncurryC2’: uncurryC2 = Dict
    • Relevant bindings include
        uncurryC2 :: Dict (Implies (a, b) c) (bound at Bug.hs:27:1)
   |
27 | uncurryC2 = Dict
   |             ^^^^

All of these uncurryC-functions typecheck except for uncurryC2. (Note that the first two require ImpredicativeTypes, so I'm not sure if this is intended to be supported or not.)

comment:2 Changed 19 months ago by simonpj

In uncurryC2 we have a given

[G] Implies a (Implies b c)

by taking its superclass we also have

[G] forall. a => Implies b c

But now we are stuck because I have not yet implemented the superclass story for quantified constraints.

comment:3 Changed 19 months ago by Iceland_jack

With the latest changes uncurryC2 works. Should this be closed?

comment:4 Changed 19 months ago by simonpj

Yes; and I've added a test case

commit 32e8499889d314e9efd0747b4053290a2dc237d5
Author: Simon Peyton Jones <simonpj@microsoft.com>
Date:   Fri Mar 2 22:53:27 2018 +0000

    Test Trac #14863

comment:5 Changed 19 months ago by simonpj

Resolution: fixed
Status: newclosed

comment:6 Changed 19 months ago by Iceland_jack

This is great work thanks!

For those interested these examples came from Edward Kmett's encoding of sums of Constraints. This may be a milestone, since curryC / uncurryC mean that the "category of entailment" (:-) is a Cartesian closed (Constraint) category (which means we could get HOAS syntax for constraints?).

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

comment:7 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed

comment:8 Changed 16 months ago by RyanGlScott

Milestone: 8.6.1
Test Case: quantified-constraints/T14863
Note: See TracTickets for help on using tickets.