🐛 Fix: Type Variable Shadowing Error

Motivation and Context

Related Issue: #1512 (closed)

Diagnosis: evaluate_type was preferring declared types over type variables introduced by E_type_abstraction/T_for_all/T_abstractions. This was due to the following code in evaluate_type:

let rec evaluate_type (type_ : I.type_expression) : (Type.t, 'err, 'wrn) C.t =
  ... 
  | T_variable tvar ->
    (match%bind Context.get_type tvar with
    | Some type_ -> lift type_
    | None ->
      (match%bind Context.get_type_var tvar with
      | Some _ -> const @@ T_variable tvar
      | None -> raise (unbound_type_variable tvar)))

This was resulting in the following code:

type a = int
let id (type a) (x : a) : a = x

having the following typed representation:

$ dune exec ligo -- print ast-typed wat2.mligo
type a = int                                
const id : ∀ a : * . int -> int = Λ a ->  fun ( xintint) -> x

Description

The fix is fairly simple. Modified Computation and Context to provide a get_type_or_type_var function.

(* computation.mli *)
...
module Context : sig
  ...

  (** [get_type_or_type_var tvar] returns the type or kind of the type variable [tvar].
      Returning [None] if not found in the current context. *)
  val get_type_or_type_var
    :  Type_var.t
    -> ([ `Type of Type.t | `Type_var of Kind.t ] option, 'err, 'wrn) t

  val get_type_or_type_var_exn
    :  Type_var.t
    -> error:'err Errors.with_loc
    -> ([ `Type of Type.t | `Type_var of Kind.t ], 'err, 'wrn) t

end

The associated code in evaluate_type is then modified to call this function:

  | T_variable tvar ->
    (* Get the closest type or type variable with type var [tvar] *)
    (match%bind
       Context.get_type_or_type_var_exn tvar ~error:(unbound_type_variable tvar)
     with
    | `Type type_ -> lift type_
    | `Type_var _kind -> const @@ T_variable tvar)

This ensures that we always find the "closest" type or type variable bound by tvar when evaluating the type variable.

Types of changes

• Bug fix (non-breaking change which fixes an issue)
• New feature (non-breaking change which adds functionality)
• Breaking change (fix or feature that would cause existing functionality to not work as expected)
• Performance improvement (non-breaking change that improves performance)
• None (change with no changelog)

Changelog

Fixed type variable shadowing issues.

Checklist:

• Changes follow the existing coding style (use dune fmt to check).
• Tests for the changes have been added (for bug fixes / feature).
• Documentation has been updated.
• Changelog description has been added (if appropriate).
• Start titles under ## Changelog section with #### (if appropriate).
• There is no image or uploaded file in changelog
• Examples in changed behaviour have been added to the changelog (for breaking change / feature).