Template polymorphism is not implemented

[SimonBoulier]

Template polymorphism is not implemented. For template polymorphism see: refman The following compiles in Coq:

Definition T := {A : Type & {B : Type & A}}.

While it does not in Template Coq:

Require Import Template.TemplateCoqChecker.
Fail Template Check T.

I am not sure we will implement it because we can use full polymorphism instead but people should be aware of it. @mattam82 Do you confirm?

[mattam82]

Indeed, I’d rather avoid the complications but it’s not so hard to implement

[mattam82]

This should be mentionned in the manual/readme