Equality of De Bruijn-indexed variables in a GADT

Question

I have a problem convincing the compiler that two De Bruijn-indexed variables are the same. I have the following deep embeddeding of a DSL, with the De Bruijn indexing code based on Manuel Chakravarty's Converting a HOAS term GADT into a de Bruijn term GADT:

{-# LANGUAGE GADTs #-}

data Ix env t where
    ZeroIx ::             Ix (env, t) t
    SuccIx :: Ix env t -> Ix (env, s) t

-- | Heterogeneous equality for 'Ix'. Note, this only ensures that
-- the indices are equal as integers; it does not ensure that their
-- type environments are equal. (Though we do require that the types
-- of the values they're bound to to be the same, i.e. @(a ~ a)@.)
eqIx :: Ix l a -> Ix r a -> Bool
eqIx ZeroIx     ZeroIx     = True
eqIx (SuccIx m) (SuccIx n) = eqIx m n
eqIx _          _          = False

data Dist env e where
    Var        :: Ix env e -> Dist env e
    --- XXX: What should Let look like?
    ConcatMap  :: (a -> [b]) -> Dist env [a] -> Dist env [b]
    -- For sibling fusion:
    ConcatMap2 :: (a -> ([b], [c])) -> Dist env [a] -> Dist env ([b], [c])
    Fst        :: Dist env ([a], [b]) -> Dist env [a]
    Snd        :: Dist env ([a], [b]) -> Dist env [b]

fuse :: Dist env e1 -> Dist env e2 -> (Dist env e1, Dist env e2)
fuse (ConcatMap f v@(Var x)) (ConcatMap g (Var y))
    | eqIx x y = let e = ConcatMap2 (f `mapBoth` g) v
                 in (Fst e, Snd e)  -- XXX: Doesn't type check.
fuse e1 e2 = (e1, e2)

mapBoth :: (a -> [b]) -> (a -> [c]) -> a -> ([b], [c])
mapBoth = undefined

The function fuse tries to implement sibling fusion (a tupling optimization). I need to pattern match on two Vars that are the same. While I can compare the indices themselves, I also need to convince the compiler that the typing environment these indices are in is the same and they thus map to a value of the same type. I have a feeling that this might be solved by adding the Let constructor and pattern matching on it, but it's unclear to me how. Here's an abridged version of the type error:

/tmp/Minimal.hs:27:14:
    Could not deduce (a1 ~ a)
    from the context (e1 ~ [b])
      bound by a pattern with constructor
                 ConcatMap :: forall env a b.
                              (a -> [b]) -> Dist env [a] -> Dist env [b],
               in an equation for ‘fuse’
      at /tmp/Minimal.hs:26:7-27
    or from (e2 ~ [b1])
      bound by a pattern with constructor
                 ConcatMap :: forall env a b.
                              (a -> [b]) -> Dist env [a] -> Dist env [b],
               in an equation for ‘fuse’
      at /tmp/Minimal.hs:26:31-49
      ‘a1’ is a rigid type variable bound by
           a pattern with constructor
             ConcatMap :: forall env a b.
                          (a -> [b]) -> Dist env [a] -> Dist env [b],
           in an equation for ‘fuse’
           at /tmp/Minimal.hs:26:31
      ‘a’ is a rigid type variable bound by
          a pattern with constructor
            ConcatMap :: forall env a b.
                         (a -> [b]) -> Dist env [a] -> Dist env [b],
          in an equation for ‘fuse’
          at /tmp/Minimal.hs:26:7
    Expected type: Ix env [a]
      Actual type: Ix env [a1]

How can I pattern match on two variables that are the same?

Answer 1

I can make your code type-check with two relatively simple changes. However I'm not entirely sure if they're truly valid in the wider context of your entire code.

Firstly, the type of eqIx doesn't make use of the knowledge you already have, namely that the env parameters are already known to be the same when you call it. We can change it to this instead and it'll still type-check - i.e. we assume that the environments are the same but the variable types may not be.

eqIx :: Ix env a -> Ix env b -> Bool

After this change, the important thing that eqIx does tell us is that the types of the two variables are actually the same. But by only returning a Bool we're hiding this from the compiler. If we instead return a standard type-level "equality witness", we can propagate this information:

data EqWitness a b where
    IsEq :: EqWitness a a

eqIx :: Ix env a -> Ix env b -> Maybe (EqWitness a b)
eqIx ZeroIx     ZeroIx     = Just IsEq
eqIx (SuccIx m) (SuccIx n) = eqIx m n
eqIx _          _          = Nothing

(There's probably some standard type for EqWitness on hackage somewhere)

Now we can add PatternGuards and change your call-site slightly to extract the equality witness when eqIx succeeds. This makes the equality available to the type-checker in the body of the relevant case:

fuse :: Dist env e1 -> Dist env e2 -> (Dist env e1, Dist env e2)
fuse (ConcatMap f v@(Var x)) (ConcatMap g (Var y))
    | Just IsEq <- eqIx x y
               = let e = ConcatMap2 (f `mapBoth` g) v
                 in (Fst e, Snd e)
fuse e1 e2 = (e1, e2)