[Haskell] Lemmas about type functions

[Louis-Julien Guillemette]

Hi all,

I've been using GHC's type families somewhat extensively in my
type-preserving compiler (BTW, they work great), and quite often I
come across the need to prove lemmas about those functions.  As far as
I understand there's currently no way to handle such lemmas purely at
the type level, and I have to encode them as term-level functions.

I wonder if I'm missing something, or otherwise if there are plans to
provide some way to do this kind of type-level reasoning.

Here's a simple example.

I encode (de Bruijn) type contexts as lists of types of this form:

   (t0, (t1, (... , ()...)))

I sometimes concatenate type contexts, and need a lemma stating that
appending an empty context leaves it unchanged (ts ++ [] == ts).

   type family Cat ts0 ts
   type instance Cat ()      ts' = ts'
   type instance Cat (s, ts) ts' = (s, Cat ts ts')

That is, I need to coerce:

   Exp (Cat ts ())

into:

   Exp ts

The way I presently do it is through a term-level function that
produces a witness that the two types are equivalent, like this:

data Equiv s t where
  Equiv :: (s ~ t) => Equiv s t

cat_nil :: EnvRep ts -> Equiv (Cat ts ()) ts
cat_nil R0 = Equiv
cat_nil (Rs _ ts_r) = case cat_nil ts_r of Equiv -> Equiv

coerce :: EnvRep ts -> Exp (Cat ts ()) -> Exp ts
coerce ts_r e = case cat_nil ts_r of Equiv -> e


Louis