Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

#14835 closed bug (fixed)

QuantifiedConstraints: Can't deduce "(a, b)" from "a" and "b"

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: quantified-constraints/T14835
Blocked By: Blocking:
Related Tickets: #14833 Differential Rev(s):
Wiki Page:


{-# 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)

class    ((a, b) => c) => Curried a b c
instance ((a, b) => c) => Curried a b c

curryC :: forall a b c. ((a, b) |- c) :- (a |- b |- c)
curryC = Dict

This fails with

GHCi, version 8.5.20180128:  :? for help
[1 of 1] Compiling Main             ( /tmp/Test.hs, interpreted )

/tmp/Test.hs:16:10: error:
    • Could not deduce (a, b) arising from a use of ‘Dict’
      from the context: (a, b) |- c
        bound by a quantified context at /tmp/Test.hs:1:1
      or from: a bound by a quantified context at /tmp/Test.hs:1:1
      or from: b bound by a quantified context at /tmp/Test.hs:1:1
      Possible fix:
        add (a, b) to the context of
          the type signature for:
            curryC :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                      ((a, b) |- c) :- (a |- (b |- c))
    • In the expression: Dict
      In an equation for ‘curryC’: curryC = Dict
16 | curryC = Dict
   |          ^^^^
Failed, no modules loaded.

but it works by changing the type of curryC:

curryC :: forall a b c. Curried a b c :- (a |- b |- c)

Change History (3)

comment:1 Changed 19 months ago by RyanGlScott

I think this is another manifestation of #14833. Here's an analogous removal of cruft for this ticket:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# 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

curryC1 :: ((a, b) => c) => Dict (Implies a (Implies b c))
curryC1 = Dict

curryC2 :: Implies (a, b) c => Dict (Implies a (Implies b c))
curryC2 = Dict

Note that curryC1 typechecks, but curryC2 does not.

comment:2 Changed 19 months ago by simonpj

Resolution: fixed
Status: newclosed
Test Case: quantified-constraints/T14835

Yes, fixed with #14833.

comment:3 Changed 16 months ago by RyanGlScott

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