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

[Tom Ellis]

Ah yes, thanks, I see!  Actually, this version seems to be sufficient
to show the problem:

    main :: IO ()
    main = do
      putStrLn "Hi"
      applyDict#
        uncallable
        (apDict# (\_ -> error "fake dictionary") :: Dict# (Implies () (True ~ False)))
      putStrLn "Bye"

We can make the constraint `Implies () (True ~ False)` which is
neither bottom nor a correct constraint and then it's GHC itself which
solves the `()` constraint, applying it to unveil bottom; in userland
we don't get a chance to test it for bottomness.

I think there's yet some hope we could build up the constraints using
a more restrictive set of combinators, rather than (->), which would
guarantee that all constraints produced that way are either bottom or
total.  Seems to be difficult but thorny territory though.

Thanks again for your help discovering the flaw with this idea.

Tom




On Fri, Dec 01, 2023 at 06:04:53PM +0000, Li-yao Xia wrote:
> 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"