FStar doesn't have phantom types

[theolaurent]

According to the Haskell Wiki:

A phantom type is a parametrised type whose parameters do not all appear on the right-hand side of its definition

In FStar, type parameters are added as regular implicits arguments of the type constructors (for example, on can project them). So morally, they do appear on the right-hand side. This is mentioned by @kyoDralliam in #65.

I don't know if lack of phantom types is such an issue, but it seems like a weird setting to me. Anyway as projecting type parameters from constructors is about to be forbidden (fix for #65), opening this issue for discussion.

Question: maybe we shouldn't carry them around at all?

[theolaurent]

Or maybe it is just enough to forbid matching? How does it work in Coq for example?

[A-Manning]

IIRC type parameters index constructors, but you can get an erased parameter like so:

type notPhantom (a: Type) =
    | NotPhantom

type phantom (a: Type) (b: Type) = notPhantom a

[nikswamy]

Closing this issue. A-Manning's response still looks pretty good to me.