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"