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