[Haskell-cafe] Does the constraints library give (a :- b) -> Dict (a |- b)?

[Li-yao Xia]

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 at 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.