diff --git a/lib/inference.ml b/lib/inference.ml index c620ddc..f06b55c 100644 --- a/lib/inference.ml +++ b/lib/inference.ml @@ -22,6 +22,11 @@ let typeof t = (match proj with | Term.First -> Some ty1, env | Term.Second -> Some ty2, env) + | Some (Type.Var id), env' -> + (* Variable is a product *) + (match TypeSubstitution.find id env' with + | Some ty -> Some ty, env' + | None -> None, env') | _ -> None, env) | Term.Fun (id, body) -> let arg = TypeSubstitution.singleton id (Type.Var id) in