Re: [Haskell-cafe] Is UndecidableInstances unavoidable in heterogenous Show derivation?
... was mildly surprised by the need for -XUndecidableInstances when deriving the 'Show' instance for the heterogenous N-ary product 'NP':
Hi Viktor, yes 'Undecidable' sounds scary, but it isn't. There's been much debate: should we find a less scary name? Presumably your program compiles and runs OK with that switched on(?) Providing your program compiles, it is type-safe. The risk with -XUndecidableInstances is that you might throw the compiler into a loop, in which case you'll get a stack depth check, with an unhelpful error message. See the Users Guide on UndecidableInstances, also this is a faq on StackOverflow.
deriving instance All (Compose Show f) xs => Show (NP f xs)
Yes the constraint on that instance violates the Paterson Conditions (see Users Guide), the constraint is no smaller than the instance head. The P Conditions aim to make each step of instance resolution smaller, by strictly decreasing "constructors and variables (taken together ...". But that constraint has a count of 4, same as the head.
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).
[ Perhaps I should be more blasé about enabling these extensions, but I prefer to leave sanity checks enabled when possible. ]
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. There are/were several proposals to make this a per-instance or per-class pragma. But they got no support in the proposals process. AntC
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-Fa... 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.
participants (2)
-
Anthony Clayden -
Viktor Dukhovni