Opened 19 months ago

Closed 19 months ago

Last modified 16 months ago

#14878 closed bug (invalid)

Can't witness transitivity ((.)) of isomorphism of Constraints

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 compiles,

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

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

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

type a -:- b = Dict (Implies a b, Implies b a) -- isomorphism of constraints, should be an equivalence relation

id_ :: a-:-a
id_ = Dict

sym_ :: a-:-b -> b-:-a
sym_ Dict = Dict

-- comp_ :: a-:-b -> b-:-c -> a-:-c
-- comp_ Dict Dict = Dict

but uncommenting comp_ and GHC doesn't know how to deduce b (the location message is weird)

$ ghci -ignore-dot-ghci hs/206-bug-quantified-constraints.hs
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( hs/206-bug-quantified-constraints.hs, interpreted )

hs/206-bug-quantified-constraints.hs:1:1: error:
    Could not deduce: b
    from the context: (Implies a b, Implies b a)
      bound by a pattern with constructor:
                 Dict :: forall (c :: Constraint). c => Dict c,
               in an equation for ‘comp_’
      at hs/206-bug-quantified-constraints.hs:18:7-10
    or from: (Implies b c, Implies c b)
      bound by a pattern with constructor:
                 Dict :: forall (c :: Constraint). c => Dict c,
               in an equation for ‘comp_’
      at hs/206-bug-quantified-constraints.hs:18:12-15
    or from: c
      bound by a quantified context
      at hs/206-bug-quantified-constraints.hs:1:1
  |
1 | {-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
  | ^

hs/206-bug-quantified-constraints.hs:1:1: error:
    Could not deduce: b
    from the context: (Implies a b, Implies b a)
      bound by a pattern with constructor:
                 Dict :: forall (c :: Constraint). c => Dict c,
               in an equation for ‘comp_’
      at hs/206-bug-quantified-constraints.hs:18:7-10
    or from: (Implies b c, Implies c b)
      bound by a pattern with constructor:
                 Dict :: forall (c :: Constraint). c => Dict c,
               in an equation for ‘comp_’
      at hs/206-bug-quantified-constraints.hs:18:12-15
    or from: a
      bound by a quantified context
      at hs/206-bug-quantified-constraints.hs:1:1
  |
1 | {-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}
  | ^
Failed, no modules loaded.
Prelude> 

simplifying and uncurrying we get a more minimal example

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

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

f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
f = Dict

giving a different and longer error message

GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( 206-bug-quantified-constraints.hs, interpreted )

206-bug-quantified-constraints.hs:6:6: error:
    • Could not deduce: c0
      from the context: (a => b, b => a, b => c, c => b, a => c, c)
        bound by the type signature for:
                   f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                        (a => b, b => a, b => c, c => b, a => c, c) =>
                        Dict a
        at 206-bug-quantified-constraints.hs:6:6-58
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |
6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

206-bug-quantified-constraints.hs:6:6: error:
    • Could not deduce: (b, c0)
      from the context: (a => b, b => a, b => c, c => b, a => c, c)
        bound by the type signature for:
                   f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                        (a => b, b => a, b => c, c => b, a => c, c) =>
                        Dict a
        at 206-bug-quantified-constraints.hs:6:6-58
      or from: a
        bound by a quantified context
        at 206-bug-quantified-constraints.hs:6:6-58
    • In the type signature:
        f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |
6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

206-bug-quantified-constraints.hs:6:6: error:
    • Could not deduce: b0
      from the context: (a => b, b => a, b => c, c => b, a => c, c)
        bound by the type signature for:
                   f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                        (a => b, b => a, b => c, c => b, a => c, c) =>
                        Dict a
        at 206-bug-quantified-constraints.hs:6:6-58
      or from: c0
        bound by a quantified context
        at 206-bug-quantified-constraints.hs:6:6-58
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |
6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

206-bug-quantified-constraints.hs:6:6: error:
    • Could not deduce: c0
      from the context: (a => b, b => a, b => c, c => b, a => c, c)
        bound by the type signature for:
                   f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                        (a => b, b => a, b => c, c => b, a => c, c) =>
                        Dict a
        at 206-bug-quantified-constraints.hs:6:6-58
      or from: b0
        bound by a quantified context
        at 206-bug-quantified-constraints.hs:6:6-58
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |
6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

206-bug-quantified-constraints.hs:6:6: error:
    • Could not deduce: b
      from the context: (a => b, b => a, b => c, c => b, a => c, c)
        bound by the type signature for:
                   f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                        (a => b, b => a, b => c, c => b, a => c, c) =>
                        Dict a
        at 206-bug-quantified-constraints.hs:6:6-58
      or from: b0
        bound by a quantified context
        at 206-bug-quantified-constraints.hs:6:6-58
    • In the ambiguity check for ‘f’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:
        f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |
6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

206-bug-quantified-constraints.hs:6:6: error:
    • Could not deduce: (b, b0)
      from the context: (a => b, b => a, b => c, c => b, a => c, c)
        bound by the type signature for:
                   f :: forall (a :: Constraint) (b :: Constraint) (c :: Constraint).
                        (a => b, b => a, b => c, c => b, a => c, c) =>
                        Dict a
        at 206-bug-quantified-constraints.hs:6:6-58
      or from: a
        bound by a quantified context
        at 206-bug-quantified-constraints.hs:6:6-58
    • In the type signature:
        f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |
6 | f :: (a => b, b => a, b => c, c => b, a => c, c) => Dict a
  |      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.
Prelude> 

Change History (5)

comment:1 Changed 19 months ago by RyanGlScott

I don't think this is a bug. Consider this example:

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}

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

f :: ( c
     , c => d
     )
  => Dict d
f = Dict

This works, because there is exactly one matching local instance (c => d) for d. What about this example, which is closer to what you are writing?

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE QuantifiedConstraints #-}

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

f :: ( a, b
     , a => c, b => c
     , c => d
     )
  => Dict d
f = Dict

There is one matching local instance (c => d) for d, so we try to deduce c. But there are multiple matching local instances for c: a => c and b => c. Which one does GHC pick? As noted in the quantified constraints proposal, if GHC is ever in doubt about which local instance to pick, it simply rejects the code.

comment:2 Changed 19 months ago by Iceland_jack

Resolution: invalid
Status: newclosed

Ah that's sensible, and not too difficult to work around:

{-# Language QuantifiedConstraints, GADTs, ConstraintKinds, TypeOperators, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, TypeApplications, ScopedTypeVariables #-}

import Data.Kind

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

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

type a  :- b = Dict (Implies a b)
type a -:- b = Dict (Implies a b, Implies b a)

type Iso s t a b = Dict (Implies a b, Implies s t)

comp_ :: forall a b c. a-:-b -> b-:-c -> a-:-c
comp_ Dict Dict = comp__ @c @b @a @b @a @c b1 a1 a2 b2 where

  a1 :: a:-b
  a1 = Dict

  a2 :: b:-a
  a2 = Dict

  b1 :: c:-b
  b1 = Dict

  b2 :: b:-c
  b2 = Dict

comp__ :: s:-t -> a:-b -> t:-i -> b:-c -> Iso s i a c
comp__ Dict Dict Dict Dict = Dict

comment:3 Changed 19 months ago by Iceland_jack

This can additionally be witnessed by carrying the witness and composing it explicitly

type Cat ob = ob -> ob -> Type

data ImpliesC :: Cat Constraint where
  ImpliesC :: (a => b) => ImpliesC a b

data IsoC :: Cat Constraint where
  IsoC :: ImpliesC a b -> ImpliesC b a -> IsoC a b

instance Category ImpliesC where
  id :: ImpliesC a a
  id = ImpliesC 

  (.) :: ImpliesC b c -> ImpliesC a b -> ImpliesC a c
  ImpliesC . ImpliesC = ImpliesC

instance Category IsoC where
  id :: IsoC a a
  id = IsoC id id

  (.) :: IsoC b c -> IsoC a b -> IsoC a c
  IsoC bc cb . IsoC ab ba = IsoC (bc . ab) (ba . cb)

IsoC can be parameterised by a category IsoC :: Cat ob -> Cat ob.

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

comment:4 Changed 19 months ago by Iceland_jack

To be clear this is not a bug

comment:5 Changed 16 months ago by RyanGlScott

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