Exactly how much "coinductive" constraint resolution do we do?

Summary

The following program type checks:

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

class C where
instance C => C

class D a where
instance D a => D a

class E a => E a where
instance E a

class F a => F a where
instance F a => F a

foo :: C => a
foo = undefined

bar :: D a => a
bar = undefined

baz :: E a => a
baz = undefined

quup :: F a => a
quup = undefined

I understand how operationally the dictionary is fed itself in a letrec, but does seem to undermine the notion of => as logical implication. We could have alternatively banned this, and the constraint solver would fail to terminate.

Proposed improvements or changes

I'm not sure what this could be called (hence the scare quotes on "coinductive"), what the rules are, or when/where it came about (version of GHC, paper, etc.)

Environment

• The example program is tested with 8.10