Hi Tom, There is an issue with bottoms/nontermination (which I don't see mentioned in those threads). If you have coimply :: (Dict a -> Dict b) -> Dict (a |- b), then you can apply it to (const undefined) and obtain this paradox: 1. coimply f :: Dict (a |- b) should never be bottom (const undefined is in fact a legitimate value for f: you could have b a one-method type class with one instance that's undefined). 2. If c is unsatisfiable, (d :: Dict c) must be bottom. Violating property 2 lets you "satisfy the unsatisfiable". For example, you can then apply a function of type (True ~ False) => t, which GHC expects to never be called and will in fact optimize away based on that assumption. See code below for a concrete example (which includes a plausible definition of coimply). If you can restrict the argument of coimply so as to avoid that problem, then it is plausible that you can preserve the uniqueness of instances, which seems to be the one property of type classes that we care about in Haskell (which is already broken by orphan instances and some obscure corners of overlapping instances if I recall correctly, so there is already precedent for not enforcing this property automatically). Cheers, Li-yao --- {-# LANGUAGE DataKinds, GADTs, QuantifiedConstraints, RankNTypes, UndecidableInstances, MagicHash, ScopedTypeVariables #-} module Main where import Data.Kind import GHC.Exts (Any) import Unsafe.Coerce -- Unsafe internals -- "Unboxed dictionaries" (as opposed to Dict) newtype Dict# c = Dict# Any idDict# :: forall c. c :- Dict# c idDict# = unsafeCoerce (\x -> x :: Dict# c) applyDict# :: forall c t. c :- t -> Dict# c -> t applyDict# = unsafeCoerce class (c => d) => Implies c d instance (c => d) => Implies c d apDict# :: forall c d. (Dict# c -> Dict# d) -> Dict# (Implies c d) apDict# = unsafeCoerce toDict :: Dict# c -> Dict c toDict = applyDict# ((:-) Dict) toDict# :: forall c. Dict c -> Dict# c toDict# Dict = case idDict# @c of (:-) f -> f -- Constraints library data Dict (c :: Constraint) where Dict :: c => Dict c newtype (:-) c t = (:-) (c => t) applyDict :: c :- t -> Dict c -> t applyDict ((:-) f) Dict = f -- coimply apDict :: (Dict c -> Dict d) -> Dict (Implies c d) apDict f = toDict (apDict# (toDict# . f . toDict)) -- Example (broken) usage class Unsat instance True ~ False => Unsat -- You can also just replace Unsat with True ~ False, -- which causes GHC to "optimize" away the code of uncallable to a noop uncallable :: Unsat :- a uncallable = (:-) (error "THE IMPOSSIBLE HAPPENED") fake :: Dict Unsat fake = case apDict (\_ -> error "fake dictionary") :: Dict (Implies () Unsat) of Dict -> Dict main :: IO () main = do putStrLn "Hi" applyDict uncallable fake putStrLn "Bye" On Thu, Nov 30, 2023 at 2:33 PM Tom Ellis wrote:

On Thu, Nov 30, 2023 at 01:37:47PM +0000, Tom Ellis wrote:

...

The constraints library [1] has

implied :: forall a b. (a => b) => a :- b

from which I can obtain

implied' :: Dict (a |- b) -> a :- b implied' Dict = implied

but can I get the converse of this, that is

coimplied :: (a :- b) -> Dict (a |- b) coimplied = error "Can it be done?"

I don't see how. The library itself only mentions "|-" in its definition. Would this combinator violate some guarantee that's essential for the safe use of type classes?

It seems this question has been asked at least a couple of times of the GHC bug tracker, firstly in

https://gitlab.haskell.org/ghc/ghc/-/issues/14822

where it was deemed unsound (I don't understand why) and again in

https://gitlab.haskell.org/ghc/ghc/-/issues/14937

where it remains open without having explicitly been deemed unsound.

Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

On Fri, Dec 01, 2023 at 03:46:43PM +0000, Tom Ellis wrote:

On Fri, Dec 01, 2023 at 03:03:17PM +0000, Li-yao Xia wrote:

...

There is an issue with bottoms/nontermination (which I don't see mentioned in those threads).

Yes, but can we resolve it by simply removing the possibility for bottom, e.g. by making Dict unlifted? The below code seems to be fine for example (it prints "fake dictionary"), and that only relies on making sure that the Dict# is sufficiently evaluated.

Making Dict# unlifted also seems to resolve the issue. What do you think? Is this sufficient in general to resolve the unsoundness you spotted? Tom type Dict# :: Constraint -> TYPE UnliftedRep newtype Dict# c = Dict# Any apDict# :: forall c d. (Dict# c -> Dict# d) -> Dict# (Implies c d) apDict# = unsafeCoerce id unImply# :: forall c d. Dict# (Implies c d) -> Dict# c -> Dict# d unImply# (Dict# f) (Dict# c) = Dict# (unsafeCoerce id f c) fake# :: () -> Dict# Unsat fake# () = unImply# (apDict# (\_ -> error "fake dictionary") :: Dict# (Implies () Unsat)) (toDict# Dict) main :: IO () main = do putStrLn "Hi" let !_ = applyDict uncallable (toDict (fake# ())) putStrLn "Bye"

Ah yes, thanks, I see! Actually, this version seems to be sufficient to show the problem: main :: IO () main = do putStrLn "Hi" applyDict# uncallable (apDict# (\_ -> error "fake dictionary") :: Dict# (Implies () (True ~ False))) putStrLn "Bye" We can make the constraint `Implies () (True ~ False)` which is neither bottom nor a correct constraint and then it's GHC itself which solves the `()` constraint, applying it to unveil bottom; in userland we don't get a chance to test it for bottomness. I think there's yet some hope we could build up the constraints using a more restrictive set of combinators, rather than (->), which would guarantee that all constraints produced that way are either bottom or total. Seems to be difficult but thorny territory though. Thanks again for your help discovering the flaw with this idea. Tom On Fri, Dec 01, 2023 at 06:04:53PM +0000, Li-yao Xia wrote:

Not quite. Your version uses an ad hoc unImply# to force the application, but you can already use the more general (applyDict# :: ((c => d) => t) -> Dict# (Implies c d) -> t) to lift the implication itself as a constraint (c => d), which GHC then wrongly assumes to be "well-defined" by construction. See example below. I think your idea of making things stricter is going in the right direction, but the laziness that you need to get rid of seems deeply ingrained in GHC.

---

type Dict# :: Constraint -> TYPE UnliftedRep newtype Dict# c = Dict# Any

uncallable :: (True ~ False) :- a uncallable = (:-) (error "THE IMPOSSIBLE HAPPENED")

main :: IO () main = do putStrLn "Hi" applyDict# ((:-) (case uncallable of (:-) f -> f)) (apDict# (\_ -> error "fake dictionary") :: Dict# (Implies (Implies () ()) (True ~ False))) putStrLn "Bye"

On Fri, Dec 1, 2023 at 4:13 PM Tom Ellis wrote:

...

On Fri, Dec 01, 2023 at 03:46:43PM +0000, Tom Ellis wrote:

...

On Fri, Dec 01, 2023 at 03:03:17PM +0000, Li-yao Xia wrote:

...

There is an issue with bottoms/nontermination (which I don't see mentioned in those threads).

Yes, but can we resolve it by simply removing the possibility for bottom, e.g. by making Dict unlifted? The below code seems to be fine for example (it prints "fake dictionary"), and that only relies on making sure that the Dict# is sufficiently evaluated.

Making Dict# unlifted also seems to resolve the issue. What do you think? Is this sufficient in general to resolve the unsoundness you spotted?

Tom

type Dict# :: Constraint -> TYPE UnliftedRep newtype Dict# c = Dict# Any

apDict# :: forall c d. (Dict# c -> Dict# d) -> Dict# (Implies c d) apDict# = unsafeCoerce id

unImply# :: forall c d. Dict# (Implies c d) -> Dict# c -> Dict# d unImply# (Dict# f) (Dict# c) = Dict# (unsafeCoerce id f c)

fake# :: () -> Dict# Unsat fake# () = unImply# (apDict# (\_ -> error "fake dictionary") :: Dict# (Implies () Unsat)) (toDict# Dict)

main :: IO () main = do putStrLn "Hi" let !_ = applyDict uncallable (toDict (fake# ())) putStrLn "Bye"