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.
