[Haskell-cafe] Is UndecidableInstances unavoidable in heterogenous Show derivation?
ietf-dane at dukhovni.org
Sun Dec 1 04:06:00 UTC 2019
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(?)
> > 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:
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
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.
More information about the Haskell-Cafe