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 <tom-lists-haskell-cafe-2023@jaguarpaw.co.uk> 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" _______________________________________________ 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.