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
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" _______________________________________________ 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.