Could Not Deduce with Dependent Typing

Question

I've been playing around with some cofree isomporphisms with dependent typing, and am getting an error message that just seems to be nonsense for me.

My dependently typed cofree

data Cofree (n :: Nat) f a where
  (:<<) :: a -> f (Cofree n f a) -> Cofree ('S n) f a

and isomorphism code

class Iso a b where
  toA :: b -> a
  toB :: a -> b

and my (very basic) instance (it's missing a lot of stuff but I want to just take care of the basics first)

instance Iso (Vec ('S n) a) (Cofree ('S n) Maybe a) where
  toA :: Cofree ('S n) Maybe a -> Vec ('S n) a
  toA (x :<< Nothing) = VCons x VNil

I figured that'd be the most basic thing possible, but it still type errors.

The error itself:

interactive>:224:127: error:
    * Could not deduce: n1 ~ 'Z
      from the context: 'S n ~ 'S n1
        bound by a pattern with constructor:
               :<< :: forall (f :: * -> *) a (n :: Nat).
                      a -> f (Cofree n f a) -> Cofree ('S n) f a,
             in an equation for `toA'
    at <interactive>:224:112-122
  `n1' is a rigid type variable bound by
    a pattern with constructor:
      :<< :: forall (f :: * -> *) a (n :: Nat).
             a -> f (Cofree n f a) -> Cofree ('S n) f a,
    in an equation for `toA'
    at <interactive>:224:112
  Expected type: Vec ('S n) a
    Actual type: Vec ('S 'Z) a
* In the expression: VCons x VNil
  In an equation for `toA': toA (x :<< Nothing) = VCons x VNil
  In the instance declaration for
    `Iso (Vec ('S n) a) (Cofree ('S n) Maybe a)'

which seems weird, since I don't get why it can't substitute 'Z in for n1 in the type equation, since that seems to solve it.

I tried doing the hole thing (so instead in my definition I had:

= _ $ VCons x VNil

which returned

 Found hole: _ :: Vec ('S 'Z) a -> Vec ('S n) a

which seems weird, since why couldn't I just supply id in there, it matches 'Z with n, and boom, solved?

By the way, the definitions for Nat and Vec I think are pretty normal so I didn't want to clutter up this post with more code than I needed, so I can provide them if it would be easier for somebody.

EDIT: The Nat I used was

data Nat = Z | S Nat

and the Vec I used was

data Vec (n :: Nat) a where
  VNil :: Vec 'Z a
  VCons :: a -> Vec n a -> Vec ('S n) a

and no imports necessary, but GADTs, DataKinds, MultiParamTypeClasses, KindSignatures, and FlexibleInstances are necessary, and maybe PolyKinds? I don't quite remember.

BTW data Iso a b = Iso { toA :: b -> a, toB :: a -> b } will serve you much better than your class -- not in solving this problem, just in general. — luqui
Vec ('S n) a and Cofree ('S n) Maybe a are not isomorphic, so you'll have quite a bit of difficulty proving they are. — user2407038
Please provide an MCVE with the right imports, language extensions, etc. — gallais
@luqui Why is that data structure more useful? Classes seem more intuitive to me, but my intuition could definitely be wrong on this (I'm a bit of a beginner). — Eliza Brandt
@gallais Thank you for the link, that was very useful. I think I've added everything I needed. — Eliza Brandt

gallais gallais · Accepted Answer · 2017-12-14T17:33:19

The problem here is that you may pick Maybe's Nothing constructor whenever you want but you can only use Vec's VNil constructor when the index is Z. This mismatch makes the isomorphism impossible to implement.

You can however salvage the situation by:

changing the definition of indexed Cofree so that its argument f is also indexed
introducing a variant of Maybe where you may only use the Nothing constructor when the index is Z

In other words:

data ICofree (n :: Nat) f a where
  (:<<) :: a -> f n (ICofree n f a) -> ICofree ('S n) f a

data IMaybe (n :: Nat) a where
  INothing :: IMaybe 'Z a
  IJust    :: a -> IMaybe ('S n) a

instance Iso (Vec n a) (ICofree n IMaybe a) where
  toA (x :<< INothing) = VCons x VNil
  toA (x :<< IJust xs) = VCons x (toA xs)

  toB (VCons x VNil)       = x :<< INothing
  toB (VCons x xs@VCons{}) = x :<< IJust (toB xs)

And a self-contained gist with the right imports, language extensions and definitions.

Could Not Deduce with Dependent Typing

2 Answers