Type synonym definitions with non-type arguments should give an error.

[lukaszcz]

Currently, the definition

f : Nat → Type;
f zero := Nat;
f (suc _) := Bool;

type checks. However, it cannot be used. For example,

h : f zero := zero;

gives the error:

The expression zero has type:
  Nat
but is expected to have type:
  f zero

Since f cannot be used, it will be filtered out by reachability analysis. But the type signature of f should give a type error, because it's not really supported and translating f to Core is erroneous at this point, because the well-typedness assumptions in the Core pipelines don't support such type synonym definitions.