The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hi, Nico --

I don't believe this is possible. If the type is embedded inside of a term, then that term could be opened up via Ltac, and then Ltac could construct a term using constr and avoid your check.

It is possible to express your restriction via arguments? For example, if you want a type function that requires a type with a decidable equality there are several ways to do it:

(* type class *)

Class EqDec (T : Type) : Type :=

{ eq_dec : forall a b : T, {a = b} + {a <> b} }.

Axiom M : forall T : Type, EqDec T -> Type.

(* using a record/canonical structure *)

Record dtype : Type := { type : Type ; dec : forall a b : type, {a = b} + {a <> b}).

Axiom M : dtype -> Type.

If there is something more complex/restrictive, you could also get away with a deep encoding of the syntax, something like:

(* using a deep embedding of the syntax of types *)

Inductive Only_Nat_Arrow : Type := Nat | Arr (_ _ : Only_Nat_Arrow).

Fixpoint ONAD (a : Only_Nat_Arrow) : Type :=

   match a with

   | Nat => nat

   | Arr a b => ONAD a -> ONAD b

  end.

Axiom M : Only_Nat_Arrow -> Type.

Hope this helps.

On Fri, May 15, 2015 at 7:36 AM, Nico <nlehmann AT dcc.uchile.cl> wrote:

Hi all,

I want to write a plugin that expose a type that can be introduced only by a ocaml tactic that check if the parameters of the type satisfies a structural constraint regarding the axioms on which it relies.

If I hide the implementation of the type using type modules I cannot access the type constructor on the tactic, and thus cannot introduce the type.

Is there a way in which I can access a member not exposed in the module type through a ocaml tactic?

Thanks

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/