Type Deconstruction

Question

My data types will always have at least two parameters, and the last two parameters are always 'q' and 'm', respectively:

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, ConstraintKinds, FlexibleInstances #-}

data D1 q m = D1 q
data D2 t q m = D2 q

class Foo a where -- a has kind * -> *
   f :: a x -> a x

class (Foo b) => Bar b where -- b has kind * -> *
   -- the purpose of g is to change ONE type parameter, while fixing the rest
   -- the intent of the equality constraints is to decompose the parameter b into
   -- its base type and 'q' parameter, then use the same base type with a *different*
   -- `q` parameter for the answer
   g :: (b ~ bBase q1, b' ~ bBase q2) => b m -> b' m

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where
   g (D2 q) = D2 $ fromIntegral q -- LINE 1

This program results in the error

Could not deduce (bBase ~ D2 t0) (LINE 1)

When I wrote the instance, I certainly intended bBase ~ D2 t. I guess t is not bound somehow (hence the introduction of t0), and I don't know if GHC can deconstruct this type at all. Or maybe I'm just doing something silly.

More to the point, this kind of type equality/type deconstruction wouldn't be necessary if I make the parameter to Bar have kind * -> * -> *. But then I couldn't enforce the Foo constraint:

class (Foo (b q)) => Bar b where -- b has kind * -> * -> *
  g :: b q m -> q b' -- this signature is now quite simple, and I would have no problem implementing it

This won't work because q is not a parameter to Bar, and I don't want it to a parameter to Bar.

I found a solution using TWO extra "dummy" associated types, but I don't really like having them around if I don't need them:

class (Foo b, b ~ (BBase b) (BMod b)) => Bar b where -- b has kind * -> *
  type BBase b :: * -> * -> *
  type BMod b :: *

  g :: (Qux (BMod b), Qux q') => b m -> (BBase b) q' m

instance (Foo (D2 t q), Integral q) => Bar (D2 t q) where
  type BBase (D2 t q) = D2 t
  type BMod (D2 t q) = q

  g (D2 q) = D2 $ fromIntegral q

This works, but it amounts to explicitly deconstructing the type, which I think should be unnecessary given the simple type of the instance.

I'm looking for a solution to either approach: either tell me how I can enforce a class constraint on a "more-applied" type, or tell me how to make GHC deconstruct types.

Thanks!

The full error message I get is amy16.hs:7:1: Illegal equational constraint b ~ bBase q1 (Use -XGADTs or -XTypeFamilies to permit this) When checking the class method: g :: forall (bBase :: * -> * -> *) q1 (b' :: * -> *) q2 m. (b ~ bBase q1, b' ~ bBase q2) => b m -> b' m In the class declaration for Bar' Failed, modules loaded: none.` So I think you need to add either the GADTs language pragma or the TypeFamilies pragma, and possibly some other pragmas as well. — mhwombat
I didn't include the compile flags/language pragmas in the code above, but of course I'm using everything I need in those terms (which should make all of the snippets work): TypeFamilies, FlexibleContexts, UndecidableInstances, TypeOperators, DataKinds, ConstraintKinds, FlexibleInstances — crockeea

dorchard dorchard · Accepted Answer · 2013-01-30T13:45:22

From what you describe, you have types b' :: * -> * -> * for which you wish to constrain the applied b' t :: * -> * (for all t).

As you summise, you either need to deconstruct a type, which is your attempt here starting from a b :: * -> * assumed to be the result of a type application b = b' t, or to enforce a constraint on a "more-applied" type, instead from the start-point of a b' :: * -> * -> *.

Deconstructing a type is not possible, since the compiler does not know if b is even "deconstructable". Indeed, it may not be, e.g., I can make an instance instance Bar Maybe, but Maybe cannot be deconstructed into a type b' :: * -> * -> * and some type t :: *.

Starting instead from a type b' :: * -> * -> *, the constraints on an application of b' can be moved into the body of the class, where the variables are quantified:

  class Bar (b :: * -> * -> *) where
      g :: (Foo (b q1), Foo (b q2)) => b q1 m -> b q2 m

For your example there is one further wrinkle: q1 and q2 may have their own constraints, e.g. for the D2 instance you require the Integral constraint. However, Bar fixes the constraints on q1 and q2 for all instances (in this case the empty constraint). A solution is to use "constraint-kinded type families" which allow instances to specify their own constraints:

  class Bar (b :: * -> * -> *) where
      type Constr b t :: Constraint
      g :: (Foo (b q1), Foo (b q2), Constr b q1, Constr b q2) => b q1 m -> b q2 m

(include {-# LANGUAGE ConstraintKinds #-} and import GHC.Prim)

Then you can write your D2 instance:

   instance Bar (D2 t) where
      type Constr (D2 t) q = Integral q
      g (D2 q) = D2 $ fromIntegral q

Type Deconstruction

1 Answers