Constructor return type can not have holes in it

[jonaprieto]

The following program exhibits the issue. No error should be thrown.

module example;
inductive T (A : Type) {
c : T _;
};
end;

However, this is what we get:

$ juvix microjuvix typecheck example.juvix
/home/jonaprieto/example.juvix:4:5-8: error:
The constructor c has the wrong return type:
  T _
but is expected to have type:
  T A

[janmasrovira]

In my opinion we should not worry about holes in constructor return types until we properly deal with gadts. I think that in the current type system, using a hole in a constructor return type should not be supported.