Using a quantified type equality constraint from the instance constraints

Question

To set the scene, here are a bunch of language extensions we'll use, and some simplified definitions from CLaSH:

{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies, FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}

data Signal dom a
instance Functor (Signal dom) where
instance Applicative (Signal dom) where

class Bundle a where
    type Unbundled dom a = res | res -> dom a

    bundle :: Unbundled dom a -> Signal dom a
    unbundle :: Signal dom a -> Unbundled dom a

I would like to make Bundle instances for an n-ary product type. The type itself is defined as follows:

import Control.Monad.Identity

data ProductF (f :: * -> *) (ts :: [*]) where
    NilP :: ProductF f '[]
    ConsP :: f a -> ProductF f ts -> ProductF f (a : ts)
deriving instance (Show (f t), Show (ProductF f ts)) => Show (ProductF f (t : ts))

headPF :: ProductF f (t : ts) -> f t
headPF (ConsP x xs) = x

tailP :: ProductF f (t : ts) -> ProductF f ts
tailP (ConsP x xs) = xs

-- Utilities for the simple case    
type Product = ProductF Identity

infixr 5 ::>    
pattern (::>) :: t -> Product ts -> Product (t : ts)
pattern x ::> xs = ConsP (Identity x) xs

headP :: Product (t : ts) -> t
headP (x ::> xs) = x

What I would like to write is a Bundle instance that simply replaces Identity with Signal dom. Unfortunately, we can't do that in one go:

instance Bundle (Product ts) where
    type Unbundled dom (Product ts) = ProductF (Signal dom) ts

    bundle NilP = pure NilP
    bundle (ConsP x xs) = (::>) <$> x <*> bundle xs

    unbundle = _ -- Can't implement this, since it would require splitting on ts

Here, unbundle needs to do something different for ts ~ [] and for ts ~ t : ts'. OK, so let's try writing it in two instances:

instance Bundle (Product '[]) where
    type Unbundled dom (Product '[]) = ProductF (Signal dom) '[]

    bundle NilP = pure NilP
    unbundle _ = NilP

instance (Bundle (Product ts), forall dom. Unbundled dom (Product ts) ~ ProductF (Signal dom) ts) => Bundle (Product (t : ts)) where
    type Unbundled dom (Product (t : ts)) = ProductF (Signal dom) (t : ts)

    bundle (ConsP x xs) = (::>) <$> x <*> bundle xs
    unbundle xs = ConsP (headP <$> xs) (unbundle $ tailP <$> xs)

And so it is in that second instance that the problem arises. Even though we have a (quantified) type equality forall dom. Unbundled dom (Product ts) ~ ProductF (Signal dom) ts in the instance constraints, GHC 8.6.3 doesn't use it during typechecking:

For bundle:

• Couldn't match type ‘Unbundled dom (Product ts)’
                 with ‘ProductF (Signal dom) ts’
  Expected type: Unbundled dom (Product ts)
    Actual type: ProductF (Signal dom) ts1
• In the first argument of ‘bundle’, namely ‘xs’
  In the second argument of ‘(<*>)’, namely ‘bundle xs’
  In the expression: (::>) <$> x <*> bundle xs

For unbundle:

• Couldn't match expected type ‘ProductF (Signal dom) ts’
              with actual type ‘Unbundled dom (ProductF Identity ts)’
• In the second argument of ‘ConsP’, namely
    ‘(unbundle $ tailP <$> xs)’
  In the expression: ConsP (headP <$> xs) (unbundle $ tailP <$> xs)
  In an equation for ‘unbundle’:
      unbundle xs = ConsP (headP <$> xs) (unbundle $ tailP <$> xs)

A possible workaround

Of course, we can just take the long road instead: make our own class specifically for Product and delegate all the real work to that. I am presenting that solution here, but I am specifically interested in something that is less verbose and ad-hoc than this.

class IsProduct (ts :: [*]) where
    type UnbundledProd dom ts = (ts' :: [*]) | ts' -> dom ts

    bundleProd :: Product (UnbundledProd dom ts) -> Signal dom (Product ts)
    unbundleProd :: Signal dom (Product ts) -> Product (UnbundledProd dom ts)

instance (IsProduct ts) => Bundle (Product ts) where
    type Unbundled dom (Product ts) = Product (UnbundledProd dom ts)

    bundle = bundleProd
    unbundle = unbundleProd

and then IsProduct has the advantage that it can actually be implemented:

type (:::) (name :: k) (a :: k1) = (a :: k1)

instance IsProduct '[] where
    type UnbundledProd dom '[] = dom ::: '[]

    bundleProd NilP = pure NilP
    unbundleProd _ = NilP

instance (IsProduct ts) => IsProduct (t : ts) where
    type UnbundledProd dom (t : ts) = Signal dom t : UnbundledProd dom ts

    bundleProd (x ::> xs) = (::>) <$> x <*> bundleProd xs
    unbundleProd xs = (headP <$> xs) ::> (unbundleProd $ tailP <$> xs)

score 2 · Answer 1 · answered Mar 16 '19 at 05:09

The equality encodes the fact that in both cases '[] and t ': ts, the Unbundled family is defined as a ProductF. A simpler way is to not pattern-match on the list before producing that ProductF. This involves splitting out the Unbundled family of the class:

type family Unbundled dom a = res | res -> dom a
class Bundle a where
    bundle :: Unbundled dom a -> Signal dom a
    unbundle :: Signal dom a -> Unbundled dom a

So you can use a single type instance for both class instances:

type instance Unbundled dom (Product ts) = ProductF (Signal dom) ts
instance Bundle (Product '[]) where
    bundle NilP = pure NilP
    unbundle _ = NilP

instance (Bundle (Product ts), forall dom. Unbundled dom (Product ts) ~ ProductF (Signal dom) ts) => Bundle (Product (t : ts)) where
    bundle (ConsP x xs) = (::>) <$> x <*> bundle xs
    unbundle xs = ConsP (headP <$> xs) (unbundle $ tailP <$> xs)

Unfortunately, the definition of `Bundle` comes from the CLaSH prelude itself, so I can't (easily) change that. — Cactus, Mar 16 '19 at 05:12

HTNW · Accepted Answer · 2019-03-17T01:58:27.077

Well, the principled solution would be singletons:

-- | Reifies the length of a list
data SLength :: [a] -> Type where
   SLenNil :: SLength '[]
   SLenCons :: SLength xs -> SLength (x : xs)

-- | Implicitly provides @kLength@: the length of the list @xs@
class KLength xs where kLength :: SLength xs
instance KLength '[] where kLength = SLenNil
instance KLength xs => KLength (x : xs) where kLength = SLenCons kLength

The core idea (one of them, at least) behind singletons is that the implicit singleton class KLength can factor out the need for ad-hoc classes like yours. The "classiness" goes into KLength, where it can be reused; the "caseiness" goes into a literal case, and SLength is the data type gluing them together.

instance KLength ts => Bundle (Product ts) where
    type Unbundled dom (Product ts) = ProductF (Signal dom) ts

    bundle = impl
        -- the KLength xs constraint is unnecessary for bundle
        -- but the recursive call would still need it, and we wouldn't have it
        -- there's a rather unholy unsafeCoerce trick you can pull
        -- but it's not necessary yet
        where impl :: forall dom us. ProductF (Signal dom) us -> Signal dom (Product us)
              impl NilP = pure NilP
              impl (ConsP x xs) = (::>) <$> x <*> impl xs

    unbundle = impl kLength
        -- impl explicitly manages the length of the list
        -- unbundle just fetches the length of ts from the givens and passes it on
        where impl :: forall dom us. SLength us -> Signal dom (Product us) -> ProductF (Signal dom) us
              impl SLenNil _ = NilP
              impl (SLenCons n) xs = ConsP (headP <$> xs) (impl n $ tailP <$> xs)

I thought that because the constructors of `ProductF` are already in a one-to-one correspondence with the constructors of its index, it can be effectively "its own singleton". But of course now I see that the problem is that from a `Signal dom (Product ts)` we can't make a `Product ts`, but we can make an `SLength ts`. — Cactus, Mar 16 '19 at 12:26
Note that your implementation of `bundle` doesn't typecheck; it needs to be written in the same style as `unbundle`, i.e. by recursing over an `SLength`. — Cactus, Mar 16 '19 at 12:26
@Cactus Well, `bundle` does need to be written like `unbundle`, but not the way you were thinking. Also, no, the `SLength` is not being made from the `Signal dom (Product ts)`. It's given by the superclass. — HTNW, Mar 17 '19 at 02:02
well it's made from just the type of the `Signal dom (Product ts)`, which is what I meant. — Cactus, Mar 17 '19 at 02:08

Using a quantified type equality constraint from the instance constraints

A possible workaround

2 Answers2