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

1 Dec 2023

      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"