[Haskell-cafe] Is UndecidableInstances unavoidable in heterogenous Show derivation?

[Viktor Dukhovni]

On Sun, Dec 01, 2019 at 03:36:58PM +1300, Anthony Clayden wrote:

> > ... was mildly surprised by the need for -XUndecidableInstances when
> > deriving the 'Show' instance for the heterogenous N-ary product
> > 'NP':
> 
> There's been much debate: should we find a less scary name?

Perhaps, though the old name would have to stick around as an alias for
a few major releases.  But if the idea is to discourage the use of the
extension when not essential, it's working! :-)

> Presumably your program compiles and runs OK with that switched on(?)

Yes.

> > I guess I should also ask whether there's a way to define something
> > equivalent to 'Compose' without 'UndecidableSuperClasses', and
> > perhaps the two are not unrelated.
>
> Not exactly related, but again superclass instance resolution wants to
> make the problem smaller at each step. The definition for class
> Compose has a constraint no smaller than the class head (3 variables).

What surprises me about 'Compose' is that it is not really trying to
define a class as such, rather it aims to construct a new constraint
(family) from an existing one.  The definition feels like a subtle hack,
used only for lack of a more natural syntax:

    http://hackage.haskell.org/package/type-combinators-0.2.4.3/docs/src/Type-Family-Constraint.html#Comp

    class d (c a) => Comp (d :: l -> Constraint) (c :: k -> l) (a :: k)
    instance d (c a) => Comp d c a

I'd have expected instead something more akin to:

    type family Comp2 (c :: l -> Constraint) (f :: k -> l) :: k -> Constraint where
        Comp2 c f = \x -> c (f x) -- Oops, no type-level lambdas
        -- or
        Comp2 c f x = c (f x)     -- Oops, too many LHS parameters

but there seems to be no direct way to express this type of composite
constraint, without inventing the clever paired class and instance.

While I can write:

    type family Comp2 (c :: l -> Constraint) (f :: k -> l) (x :: k) :: Constraint where
        Comp2 c f x = c (f x)

And partial application of Comp2 even has the expected kind:

    λ> :k Comp2 Show (K Int)
    Comp2 Show (K Int) :: k -> Constraint

sadly, one can't actually use "Comp2 Show f":

    λ> deriving instance All (Comp2 Show f) xs => Show (NP f xs)

        • The type family ‘Comp2’ should have 3 arguments, but has been given 2
        • In the context: All (Comp2 Show f) xs
          While checking an instance declaration
          In the stand-alone deriving instance for
            ‘All (Comp2 Show f) xs => Show (NP f xs)’

So the class/instance pair seems to be the only way.

> Yes that's a sensible policy. The trouble with -XUndecidableInstances
> is that it's a module-wide setting, so lifts the check for all
> instances of all classes.

So it seems best to isolate the code that needs this in as a small
module as possible, and do without everywhere else.

-- 
    Viktor.