gistfile1.txt

Require Import ZArith FMapPositive.
Open Scope positive.

(* -------- Works, but does not keep variables apart ------ *)
Definition const_t : Set := positive.
Definition var_t   : Set := positive.
Opaque const_t var_t.

Inductive ex1 : Set :=
    | ex1_const        : const_t -> ex1
    | ex1_var          : var_t -> ex1
    | ex1_const_map    : PositiveMap.t ex1 -> ex1.

Check (eq_refl : var_t = const_t).
Definition f (x : const_t) : var_t := x. (* I want this to fail *)
Definition one : var_t := 1.
Check (f one). (* I want this to fail. *)

(* -------- Does not work, but keeps variables apart ----- *)

Module Type UNIT.
End UNIT.

Module UU : UNIT.
End UU.

Module Type NAME.
    Parameter t : Set.
    Parameter map_t : Set -> Set.
    Parameter from_pos : positive -> t.
End NAME.

Module NEW_NAME (U : UNIT) : NAME.
    Definition t := positive.
    Definition map_t (A : Set) := PositiveMap.t A.
    Definition from_pos (x : positive) := x.
End NEW_NAME.

Module CONST := NEW_NAME(UU).
Module VAR := NEW_NAME(UU).

Transparent CONST.t CONST.map_t VAR.t VAR.map_t.
(* Temporarily making them transparent does not help for the inductive def. *)

Inductive ex2 : Set :=
    | ex2_const     : CONST.t -> ex2
    | ex2_var       : VAR.t -> ex2
    (* | ex2_const_map : CONST.map_t ex2 -> ex2 *)  (* non strictly positive *)
    .

Definition one2 : VAR.t := VAR.from_pos 1.
(* The good parts is that these fail type checking: *)

(* Definition f2 (x : CONST.t) : VAR.t := x.  *)

Definition g2 (x : CONST.t) : CONST.t := x.
(* Check (g2 one2). *)

(* Check (eq_refl : CONST.t = VAR.t). *)