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 <tom-lists-haskell-cafe-2023@jaguarpaw.co.uk> 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.