Georges Gonthier and François Garillot are doing interesting things with phantom types and unification in Coq to allow one to write, for example, `directv (V + W)` to mean the proposition that $V \oplus W$ is a direct sum.

I haven't fully grasped how it works yet, but let me give you a simplified explanation of what I think is going on.  What is happening is that `directv X` is really notation for `directv_def _ (Phantom _ X)`.

`Phantom` is a constructor of a very trivial inductive type

    Inductive phantom (A:Type) (a:A) : Type := Phantom : phantom A a

The function `Phantom` is a polymorphic constructor of type `forall (A:Type)(a:A), phantom A a`.  The purpose of `Phantom` is to lift values to the type level so that type inference can operate on these values.

`directv_def` doesn't even use the `(Phantom _ X)` argument (because it contains no data).  The only purpose of this argument is to drive the type inference engine to fill in the first argument.  `directv_def` has type `forall (VW : addv_expr) (_ : phantom _ (Vadd VW)), Prop`.  `addv_expr` is a record type.

    Record addv_expr := build_addv_expr {
     V1 : VectorSpace; 
     V2 : VectorSpace;
     Vadd : VectorSpace }

The definition of `directv_def` is

    directv_def (VW : addv_expr) _ := dim (V1 VW) + dim (V2 VW) = dim (Vadd VW)

The final ingredient is that `fun V1 V2 => (build_addv_expr V1 V2 (V1 + V2))` is declared as a Canoncial Structure.

So what does Coq read when you write `directv (V + W)`?  Well it parses this as notation for

    directv_def _ (Phantom _ (V + W))

The first parameter to Phantom is the type of `(V + W)` so we can quickly fill that in to get

    directv_def _ (Phantom VectorSpace (V + W))

`Phantom VectorSpace (V + W)` has type `phantom VectorSpace (V + W)`, but `directv_def` is expecting something of type `phantom _ (Vadd _)` so it tries to unify `(V + W)` with `(Vadd _)`.  Because `Vadd` is a record projection, Coq tries to look up in its list of canonical structures to see if there are any declared whose `Vadd` field is of the form `(V + W)`.  It says, "ahha! there is!  I can use `build_addv_expr V W (V + W)`" (notice the intensional behaviour of canonical inference here).  So Coq successfully unifies `(V + W)` with `(Vadd (build_addv_expr V W (V + W))`, and this forces the first parameter of directv_def:

    directv_def (build_addv_expr V W (V + W)) (Phantom VectorSpace (V + W))

And that is it for type inference.  Later on this expression might be used, so it will start normalizing:

    dim (V1 (build_addv_expr V W (V + W))) + dim (V2 (build_addv_expr V W (V + W))) = dim (Vadd (build_addv_expr V W (V + W))) 

and then to

    dim V + dim W = dim (V + W)


If you try to write something else like `directv 0` then the canonical structure inference will fail and you will get a (probably obtuse) type error.


----------


This has been as simplified example.  In reality, `directv` is much more complicated and allows one to write `directv (\sum_(0 <= i < n) V i)` to mean $\bigoplus_{i=0}^n V_i$ is a direct sum and accepts things like `directv 0` to mean a trivial direct sum.

Matita allows you to write unification hints directly without the necessarily building canonical structures.  I suspect doing this sort of intentional inference would be easier in such a system.