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

[Tom Ellis]

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"