Equality of Indexed De Bruijn Variables in GADT

Question

I have a problem convincing the compiler that the two De Bruijn indexed variables are the same. I have the following deep inclusion of DSL, with De Bruijn indexing code based on Manuel Chakravarty Converting the term HOAS GADT to the debris 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, ie @(a ~ a)@.) eqIx :: Ix la -> Ix ra -> Bool eqIx ZeroIx ZeroIx = True eqIx (SuccIx m) (SuccIx n) = eqIx mn 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 xy = 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 fuse function tries to implement sibling fusion (search optimization). I need to combine a pattern on two Var that match. Although I can compare the indices themselves, I also need to convince the compiler that the input environment in which these indices are located is the same, and therefore they are mapped to a value of the same type. I have a feeling that this can be solved by adding the Let constructor and pattern matching on it, but it is not clear how to do this. Here's a shortened version of an error like:

 /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 match a pattern for two variables that are the same?

Answer 1

I can do code type checking with two relatively simple changes. However, I'm not quite sure if they are valid in the wider context of all your code.

Firstly, the eqIx type eqIx not use existing knowledge, namely that the env parameters are already known when you call it. We can change it to this, and it will still check the type - that is, we assume that the environments are the same, but the types of variables may not be the same.

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

After this change, it is important that eqIx tells us that the types of the two variables are actually the same. But only returning Bool , we hide it from the compiler. If instead we return the standard type equality certificate, we can distribute this information:

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

(Probably some standard type for EqWitness for a hacker somewhere)

Now we can add PatternGuards and slightly modify your site to challenge the equality witness, if eqIx successful. This makes equality available for type checking in the body of the corresponding 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 xy = let e = ConcatMap2 (f `mapBoth` g) v in (Fst e, Snd e) fuse e1 e2 = (e1, e2)