Georges Gonthier and François Garillot are doing interesting things with phantom types and unification 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) := 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.