Is UndecidableInstances unavoidable in heterogenous Show derivation?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

Is UndecidableInstances unavoidable in heterogenous Show derivation?

Viktor Dukhovni
I was reading:

    Summer School on Generic and Effectful Programming
    Applying Type-Level and Generic Programming in Haskell
    Andres Löh, Well-Typed LLP

    https://www.cs.ox.ac.uk/projects/utgp/school/andres.pdf

and trying out the various code fragments, and was mildly surprised
by the need for -XUndecidableInstances when deriving the 'Show'
instance for the heterogenous N-ary product 'NP':

    deriving instance All (Compose Show f) xs => Show (NP f xs)

Without "UndecidableInstances" I get:

    • Variable ‘k’ occurs more often
        in the constraint ‘All (Compose Show f) xs’
        than in the instance head ‘Show (NP f xs)’
      (Use UndecidableInstances to permit this)
    • In the stand-alone deriving instance for
        ‘All (Compose Show f) xs => Show (NP f xs)’

This is not related to automatic deriving, as a hand-crafted instance triggers
the same error:

    instance All (Compose Show f) xs => Show (NP f xs) where
      show Nil = "Nil"
      show (x :* xs) = show x ++ " :* " ++ show xs

Is there some other way of putting together the building blocks that avoids the
need for 'UndecidableInstances', or is that somehow intrinsic to the type of NP
construction?

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.

[ Perhaps I should be more blasé about enabling these extensions, but I prefer
  to leave sanity checks enabled when possible. ]

--
    Viktor.

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import GHC.Exts (Constraint)

-- | Map a constraint over a list of types.
type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where
    All _ '[] = ()
    All c (x ': xs) = (c x, All c xs)

-- | With @g@ a type constructor and @f@ a constraint, define @Compose f g@ as
-- a contraint on @x@ to mean that @g x@ satisfies @f@.
--
-- Requires:
--
--   'ConstraintKinds'
--   'FlexibleInstances'
--   'MultiParamTypeClasses'
--   'TypeOperators'
--   'UndecidableSuperClasses'
--
class (f (g x)) => (Compose f g) x
instance (f (g x)) => (Compose f g) x

-- | Type-level 'const'.
newtype K a b = K { unK :: a }
deriving instance Show a => Show (K a b)

-- | N-ary product over an index list of types @xs@ via an interpretation
-- function @f@, constructed as a list of elements @f x@.
--
data NP (f :: k -> *) (xs :: [k]) where
    Nil  :: NP f '[]
    (:*) :: f x -> NP f xs -> NP f (x ': xs)
infixr 5 :*

-- | If we can 'show' each @f x@, then we can 'show' @NP f xs@.
--
-- Requires: 'UndecidableInstances'
--
deriving instance All (Compose Show f) xs => Show (NP f xs)
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Is UndecidableInstances unavoidable in heterogenous Show derivation?

AntC
> ... 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

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: 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.
_______________________________________________
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.