Hello.

Can I make the following function 'subst' well-behave,
so that it can be used in the contexts where:
1) 'p' (the first argument) is assumed of type 'path', and 
  'env' (the first argument)is assumed of type '(string * tau) list;
and 
2)'p' is assumed of type 'tau', and 
  'env' is assumed of type '(string * tau) list;


    type tau = [`Root | `Apply of path * tau |`Var of string]  
    and  path = [`Root | `Apply of path * tau] 
    
    let rec subst p env = 
    	 match p with 
    	    `Root -> `Root
    	  | `Apply (p1, p2) -> `Apply(subst p1 env , subst p2 env)
    	  | `Var s -> List.assoc s env

Yet 'subst' is well-typed, 

    let sub (p : path) (env : (string * tau)) = subst p env

fails.


At first I tried to make 'subst' explicitly typed, but I could not.
'subst' would have type 'a -> (string * tau) list -> 'a,
where the type variable 'a is only instantiated to either 'tau' or 'path'.
Then, the second clause of match
	| `Apply (p1, p2) -> `Apply(subst p1 env , subst p2 env)
would be well-typed.
It seems that I need polymorphic recursion with type constraint....

Or such encoding is inherently wrong, 
and should I define 2 mutually recursive functions?


 
Best regards,
Keiko.