[Haskell-cafe] Why does this result in a runtime loop instead of a type error or typechecker loop?

[Ryan Reich]

This seems like the canonical illustration of the dangers of
UndecidableInstances.  Normally an instance of the form "instance C1 a =>
C2 a" would be forbidden specifically because it does not exclude the
possibility of some other "instance C2 a => C1 a" elsewhere that would
create a loop.  UndecidableInstances disables this check, passing off on
you (the programmer) the responsibility of ensuring that you don't actually
do this.  You did, so you get the loop, and the compiler doesn't care
because you told it not to.

The reason the instance definitions don't loop during compilation is that
the type "HasBool a => Has Bool a" conveniently furnishes a HasBool
instance whence boolL can be obtained, so the compiler doesn't need to go
looking for an instance elsewhere, and so doesn't go into an infinite
recursion with the one that's on the next line.

The reason that even the line "runRIO () $ view boolL" doesn't cause the
compiler to loop is that, although it does infer that a = (), and therefore
does tie the knot with those two instances, it doesn't actually need to
look farther than the "HasBool ()" part of "instance Has Bool () => HasBool
()" to get boolL, as the constraint is not used in selecting an instance,
and since once that instance is selected it can easily also verify that we
do have "instance Has Bool ()" in the same oblivious way.  It just happens
that the particular definition of boolL that it gets is equivalent (after
two round of substitution) to "boolL = boolL", which only loops when it is
run.

On Mon, Jul 23, 2018 at 2:10 PM, Theodore Lief Gannon <tanuki at gmail.com>
wrote:

> λ. :set -XFlexibleContexts -XFlexibleInstances -XMultiParamTypeClasses
> -XUndecidableInstances
> λ. import RIO
> λ. import Data.Has
> λ. class HasBool a where boolL :: Lens' a Bool
> λ. instance {-#OVERLAPPABLE#-} HasBool a => Has Bool a where hasLens =
> boolL
> λ. instance {-#OVERLAPPABLE#-} Has Bool a => HasBool a where boolL =
> hasLens
> λ. runRIO () $ view boolL
> ^CInterrupted.
>
> The RIO environment () doesn't contain a Bool. I can see how the
> typechecker might get lost in this, but I can compile an equivalent
> program; it loops on execution.
>
> _______________________________________________
> 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.
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20180723/a47a91b9/attachment.html>