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

[Tom Ellis]

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.

Tom



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

toDict :: Dict# c -> Dict c
toDict !d = applyDict# ((:-) Dict) d

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

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