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

[Li-yao Xia]

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 at 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.