Why does this result in a runtime loop instead of a type error or typechecker loop?

λ. :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.

It looks like you have an infinite loop created, where `hasLens = boolL`
and `boolL = hasLens`, and the two overlappable instances are each
fulfilling the constraints of the other instance.
On Tue, Jul 24, 2018 at 12:11 AM Theodore Lief Gannon
λ. :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.

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
λ. :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.
participants (3)
-
Michael Snoyman
-
Ryan Reich
-
Theodore Lief Gannon