Compare commits

...

36 Commits

Author SHA1 Message Date
Gabriel Scherer e7b8b7a66c remove the broken gitlab CI script
3 months ago
Gabriel Scherer c98638bb21 CHANGES entry on Solver errors
3 months ago
SCHERER Gabriel 547d59c1ee Merge branch 'letrec' into 'master'
3 months ago
Gabriel Scherer 3401db210c support for (non-polymorphic) 'let rec' in Infer.ml
3 months ago
Gabriel Scherer 054ca8434b client/F: support "let rec"
3 months ago
Gabriel Scherer 5471bd8d1f client/F: keep bound variable type in 'let'
3 months ago
Gabriel Scherer 3fdb9a141e support 'let rec .. in ..' in the ML parser and AST
3 months ago
SCHERER Gabriel 7a61062b78 Merge branch 'errors-with-ranges' into 'master'
3 months ago
Gabriel Scherer c00f5569d8 include all Infer errors in the testsuite
3 months ago
Gabriel Scherer 85743ed827 use an error type in the Solver as well
3 months ago
Gabriel Scherer 3df581777c consistently use 'loc' instead of 'range' to describe source locations
3 months ago
Gabriel Scherer e31e8032fa consistently emit error locations in Infer error messages
4 months ago
Gabriel Scherer 22dde290e5 include location ranges in FTypeChecker error messages
4 months ago
SCHERER Gabriel 8514e05b91 Merge branch 'env-concat' into 'master'
4 months ago
SCHERER Gabriel 2ab5a617e7 Merge branch 'master' into 'env-concat'
4 months ago
SCHERER Gabriel 95416593ec Merge branch 'variants-error-message' into 'master'
4 months ago
Olivier c47ba76407 [FTypeChecker] More informative error message (and more robust code) when typechecking variants.
4 months ago
Olivier 47283f04f4 Small improvement in a comment.
4 months ago
Olivier 1083149b06 Add tests for pattern-matching.
4 months ago
Olivier 2025ded107 [binding_pattern] add new bindings directly in the environment.
4 months ago
SCHERER Gabriel f3f73388db Merge branch 'type-equations' into 'master'
4 months ago
Olivier 5f23395b5c Add an UnboundTypeVariable error.
4 months ago
Olivier 0debfbb71b More explicit error message printing.
4 months ago
Olivier 98ea579c6a Remove unused equality check and change comments.
4 months ago
Alistair O'Brien 5bd10c668c Apply 1 suggestion(s) to 1 file(s)
4 months ago
Olivier bcb579eafc Change 'int' to more correct 'nat' in the test suite.
4 months ago
Olivier b9749e2b57 Add tests.
4 months ago
Olivier a7006dcbb8 Smart constructors in TestF.ml.
4 months ago
Olivier 66c9de7c55 Add break in printing of annotations.
4 months ago
Olivier eed3db1da6 Comments in F.ml
4 months ago
Olivier 384f9ac3c5 Add Refl / Use in System F.
4 months ago
Olivier 473521d53a Add absurd in F.
4 months ago
Olivier 784bb81952 Equality between types always uses graph translation.
4 months ago
Olivier 6946340570 Define type equalities in [Structure.ml].
4 months ago
Olivier 36980073f3 Add type equality in F.
4 months ago
Olivier 36bad208b0 Remove unused type declaration.
4 months ago

@ -1,10 +0,0 @@
include: 'https://gitlab.com/gasche/gitlab-ocaml-ci-example/-/raw/11c1d7e/.gitlab-ci.yml'
.build-matrix:
parallel:
matrix:
- OCAML_COMPILER: "4.12.0"
variables:
DUNE_DOC_TARGETS: ""

@ -2,6 +2,16 @@
## 2022/06/03
* **Incompatible** changes to the Solver error-handling logic: instead of
raising several different exceptions, the solver now raises a single Error
exception carrying a datatype indicating the error case.
All errors now consistently report the source location when
available (if it was provided when building the constraint). This
improves in particular the error-reporting behavior of our
demonstration client, which is now able to show source locations on
type-checking errors.
* Support for rigid variables, that is, variables that cannot be unified with
other rigid variables or with older flexible variables. These variables are
introduced by the new combinators `letr1` and `letrn`. The exception

@ -1,5 +1,5 @@
(* tyconstr_id is the name of an datatype constructor.
label_id is the name of a field label or data constructor. *)
(* [tyconstr_id] is the name of an datatype constructor.
[label_id] is the name of a field label or data constructor. *)
type tyconstr_id = Type of string
type label_id = Label of string
@ -46,6 +46,8 @@ module Env = struct
}
exception UnexpectedRecord
exception DeclarationNotFound of tyconstr_id
exception LabelNotFound of label_id
let empty = {
datatypes = TyConstrMap.empty;
@ -64,19 +66,17 @@ module Env = struct
labels = add_labels e.labels tdescr.labels_descr;
}
let find_label { labels ; _ } (Label l) =
LabelMap.find (Label l) labels
let find_decl { datatypes ; _ } (Type tid) =
TyConstrMap.find (Type tid) datatypes
let label_index { labels_descr ; _ } l =
let combine i ldescr = (i, ldescr.label_name) in
List.mapi combine labels_descr
|> List.find (fun (_, l') -> l = l')
|> fst
let () = ignore label_index
let find_label { labels ; _ } label =
try
LabelMap.find label labels
with Not_found ->
raise (LabelNotFound label)
let find_decl { datatypes ; _ } tid =
try
TyConstrMap.find tid datatypes
with Not_found ->
raise (DeclarationNotFound tid)
let map (type b1 b2 t1 t2)
(f : (b1, t1) decl -> (b2, t2) decl)

@ -1,5 +1,5 @@
(* tyconstr_id is the name of an datatype constructor.
label_id is the name of a field label or data constructor. *)
(* [tyconstr_id] is the name of an datatype constructor.
[label_id] is the name of a field label or data constructor. *)
type tyconstr_id = Type of string
type label_id = Label of string
@ -34,6 +34,8 @@ module Env : sig
type ('b, 't) t
exception UnexpectedRecord
exception DeclarationNotFound of tyconstr_id
exception LabelNotFound of label_id
val empty: ('b, 't) t
val add_decl: ('b, 't) t -> ('b, 't) decl -> ('b, 't) t

@ -79,21 +79,6 @@ module Nominal2deBruijn (N : Map.OrderedType) = struct
let current = current + 1 in
{ map; current }
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
bindings of [env2] shadow any binding of the same variable in [env1]. *)
let concat env1 env2 =
(* We need to shift the de Bruijn levels of [env2] (and its
[current] value) by as many bindings as there are in [env1]. *)
let shift _x in1 in2 =
match in2 with
| None -> in1
| Some lvl -> Some (env1.current + lvl)
in
{
current = env1.current + env2.current;
map = M.merge shift env1.map env2.map;
}
end
(* -------------------------------------------------------------------------- *)

@ -49,11 +49,6 @@ module Nominal2deBruijn (N : Map.OrderedType) : sig
to [slide (bump env) x]. *)
val bump: env -> env
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
bindings of [env2] shadow any binding of the same variable in [env1]. *)
val concat: env -> env -> env
end
(* -------------------------------------------------------------------------- *)

@ -4,21 +4,26 @@
(* Types. *)
(* We include recursive types [FTyMu] in the target calculus, not only because
(* We include recursive types [TyMu] in the target calculus, not only because
we might wish to support them, but also because even if we disallow them,
they can still arise during unification (the occurs check is run late), so
we must be able to display them as part of a type error message. *)
(* Types mixing ∀ and μ are difficult to compare in general. To simplify
equality checking, we do not allow under μ.
For instance :
a. μ t. a -> t is allowed
μ t . a . (a -> t) is not allowed
μ t . ( a . a) -> t is not allowed *)
(* We also include a type equality witness [TyEq]. *)
(* Nominal or de Bruijn representation of type variables and binders. The
nominal representation is more convenient when translating from ML to F,
while the de Bruijn representation is more convenient when type-checking
F. *)
type range =
Lexing.position * Lexing.position
let dummy_range : range =
Lexing.(dummy_pos, dummy_pos)
type loc = Utils.loc
type ('a, 'b) typ =
| TyVar of 'a
@ -27,6 +32,7 @@ type ('a, 'b) typ =
| TyForall of 'b * ('a, 'b) typ
| TyMu of 'b * ('a, 'b) typ
| TyConstr of ('a, 'b) datatype
| TyEq of ('a, 'b) typ * ('a, 'b) typ
and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
@ -53,31 +59,56 @@ type debruijn_datatype_env =
(* Nominal representation of term variables and binders. *)
type tevar = string
(* Nominal or de Bruijn representation of type variables and binders. *)
(* We include a term [Refl] that represents a type equality witness.
Note that it has only one type argument but is typed as a witness for
an equality between two possibly distinct types (see [TyEq] above).
[Use] is a construct that "opens" a type equality. That is, it allows us to
reason in a context where two types are assumed to be equals.
It is supposed to be used with a type equality witness as a left-hand side :
use (eq : TyEq (ty1, ty2)) in
... (* here ty1 and ty2 are assumed to be equal *)
Doing this might introduce inconsistent assumptions about types (this can
occur for example inside a pattern matching). That is why we introduce
a construct [Absurd], that can be used as a placeholder in pieces of code
with inconsistent equations in the environment and that are thus
unreachable. *)
type tevar =
string
type ('a, 'b) term =
| Var of range * tevar
| Hole of range * ('a, 'b) typ * ('a, 'b) term list
| Annot of range * ('a, 'b) term * ('a, 'b) typ
| Abs of range * tevar * ('a, 'b) typ * ('a, 'b) term
| App of range * ('a, 'b) term * ('a, 'b) term
| Let of range * tevar * ('a, 'b) term * ('a, 'b) term
| TyAbs of range * 'b * ('a, 'b) term
| TyApp of range * ('a, 'b) term * ('a, 'b) typ
| Tuple of range * ('a, 'b) term list
| Proj of range * int * ('a, 'b) term
| LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Var of loc * tevar
| Hole of loc * ('a, 'b) typ * ('a, 'b) term list
| Annot of loc * ('a, 'b) term * ('a, 'b) typ
| Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
| App of loc * ('a, 'b) term * ('a, 'b) term
| Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
| TyAbs of loc * 'b * ('a, 'b) term
| TyApp of loc * ('a, 'b) term * ('a, 'b) typ
| Tuple of loc * ('a, 'b) term list
| Proj of loc * int * ('a, 'b) term
| LetProd of loc * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of loc * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of loc * ('a,'b) typ
| Refl of loc * ('a,'b) typ
| Use of loc * ('a,'b) term * ('a,'b) term
and rec_status = Recursive | Non_recursive
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =
| PVar of range * tevar
| PAnnot of range * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of range
| PTuple of range * ('a,'b) pattern list
| PVariant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
| PVar of loc * tevar
| PAnnot of loc * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of loc
| PTuple of loc * ('a,'b) pattern list
| PVariant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
type nominal_term = (tyvar, tyvar) term
type nominal_pattern = (tyvar, tyvar) pattern
@ -90,10 +121,10 @@ type debruijn_term =
(* Constructors. *)
let ftyabs vs t =
List.fold_right (fun v t -> TyAbs (dummy_range, v, t)) vs t
let ftyapp t tys =
List.fold_left (fun t ty -> TyApp (dummy_range, t, ty)) t tys
let ftyabs ~loc vs t =
List.fold_right (fun v t -> TyAbs (loc, v, t)) vs t
let ftyapp ~loc t tys =
List.fold_left (fun t ty -> TyApp (loc, t, ty)) t tys
(* -------------------------------------------------------------------------- *)
@ -149,7 +180,10 @@ module TypeInType : DeBruijn.TRAVERSE
let env, x = extend env x in
let ty1' = trav env ty1 in
TyMu (x, ty1')
| TyEq (ty1, ty2) ->
let ty1' = trav env ty1 in
let ty2' = trav env ty2 in
TyEq (ty1', ty2')
end
(* -------------------------------------------------------------------------- *)
@ -169,36 +203,39 @@ module TypeInTerm : DeBruijn.TRAVERSE
let rec traverse lookup extend env t =
let trav env = traverse lookup extend env in
let trav_ty env ty =
TypeInType.traverse lookup extend env ty in
match t with
| Var (pos, x) ->
Var (pos, x)
| Hole (pos, ty, ts) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
let ts' = List.map (trav env) ts in
Hole (pos, ty', ts')
| Annot (pos, t, ty) ->
let t' = trav env t
and ty' = TypeInType.traverse lookup extend env ty in
and ty' = trav_ty env ty in
Annot (pos, t', ty')
| Abs (pos, x, ty, t) ->
let ty' = TypeInType.traverse lookup extend env ty
let ty' = trav_ty env ty
and t' = trav env t in
Abs (pos, x, ty', t')
| App (pos, t1, t2) ->
let t1' = trav env t1
and t2' = trav env t2 in
App (pos, t1', t2')
| Let (pos, x, t1, t2) ->
| Let (pos, rec_, x, ty, t1, t2) ->
let ty' = trav_ty env ty in
let t1' = trav env t1
and t2' = trav env t2 in
Let (pos, x, t1', t2')
Let (pos, rec_, x, ty', t1', t2')
| TyAbs (pos, x, t) ->
let env, x = extend env x in
let t' = trav env t in
TyAbs (pos, x, t')
| TyApp (pos, t, ty) ->
let t' = trav env t
and ty' = TypeInType.traverse lookup extend env ty in
and ty' = trav_ty env ty in
TyApp (pos, t', ty')
| Tuple (pos, ts) ->
let ts' = List.map (trav env) ts in
@ -215,10 +252,20 @@ module TypeInTerm : DeBruijn.TRAVERSE
and t' = trav env t in
Variant (pos, lbl, dty', t')
| Match (pos, ty, t, brs) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
let t' = trav env t
and brs' = List.map (traverse_branch lookup extend env) brs in
Match (pos, ty', t', brs')
| Absurd (pos, ty) ->
let ty' = trav_ty env ty in
Absurd (pos, ty')
| Refl (pos, ty) ->
let ty' = trav_ty env ty in
Refl (pos, ty')
| Use (pos, t, u) ->
let t' = trav env t in
let u' = trav env u in
Use (pos, t', u')
and traverse_datatype lookup extend env (tid, tyargs) =
(tid, List.map (TypeInType.traverse lookup extend env) tyargs)

@ -4,20 +4,26 @@
(* Types. *)
(* We include recursive types [FTyMu] in the target calculus, not only because
(* We include recursive types [TyMu] in the target calculus, not only because
we might wish to support them, but also because even if we disallow them,
they can still arise during unification (the occurs check is run late), so
we must be able to display them as part of a type error message. *)
(* Types mixing ∀ and μ are difficult to compare in general. To simplify
equality checking, we do not allow under μ.
For instance :
a. μ t. a -> t is allowed
μ t . a . (a -> t) is not allowed
μ t . ( a . a) -> t is not allowed *)
(* We also include a type equality witness [TyEq]. *)
(* Nominal or de Bruijn representation of type variables and binders. The
nominal representation is more convenient when translating from ML to F,
while the de Bruijn representation is more convenient when type-checking
F. *)
type range =
Lexing.position * Lexing.position
val dummy_range: range
type loc = Utils.loc
type ('a, 'b) typ =
| TyVar of 'a
@ -26,6 +32,7 @@ type ('a, 'b) typ =
| TyForall of 'b * ('a, 'b) typ
| TyMu of 'b * ('a, 'b) typ
| TyConstr of ('a, 'b) datatype
| TyEq of ('a, 'b) typ * ('a, 'b) typ
and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
@ -55,32 +62,54 @@ type debruijn_datatype_env =
(* Nominal or de Bruijn representation of type variables and binders. *)
(* We include a term [Refl] that represents a type equality witness.
Note that it has only one type argument but is typed as a witness for
an equality between two possibly distinct types (see [TyEq] above).
[Use] is a construct that "opens" a type equality. That is, it allows us to
reason in a context where two types are assumed to be equals.
It is supposed to be used with a type equality witness as a left-hand side :
use (eq : TyEq (ty1, ty2)) in
... (* here ty1 and ty2 are assumed to be equal *)
Doing this might introduce inconsistent assumptions about types (this can
occur for example inside a pattern matching). That is why we introduce
a construct [Absurd], that can be used as a placeholder in pieces of code
with inconsistent equations in the environment and that are thus
unreachable. *)
type tevar =
string
type ('a, 'b) term =
| Var of range * tevar
| Hole of range * ('a, 'b) typ * ('a, 'b) term list
| Annot of range * ('a, 'b) term * ('a, 'b) typ
| Abs of range * tevar * ('a, 'b) typ * ('a, 'b) term
| App of range * ('a, 'b) term * ('a, 'b) term
| Let of range * tevar * ('a, 'b) term * ('a, 'b) term
| TyAbs of range * 'b * ('a, 'b) term
| TyApp of range * ('a, 'b) term * ('a, 'b) typ
| Tuple of range * ('a, 'b) term list
| Proj of range * int * ('a, 'b) term
| LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Var of loc * tevar
| Hole of loc * ('a, 'b) typ * ('a, 'b) term list
| Annot of loc * ('a, 'b) term * ('a, 'b) typ
| Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
| App of loc * ('a, 'b) term * ('a, 'b) term
| Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
| TyAbs of loc * 'b * ('a, 'b) term
| TyApp of loc * ('a, 'b) term * ('a, 'b) typ
| Tuple of loc * ('a, 'b) term list
| Proj of loc * int * ('a, 'b) term
| LetProd of loc * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of loc * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of loc * ('a,'b) typ
| Refl of loc * ('a,'b) typ
| Use of loc * ('a,'b) term * ('a,'b) term
and rec_status = Recursive | Non_recursive
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =
| PVar of range * tevar
| PAnnot of range * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of range
| PTuple of range * ('a,'b) pattern list
| PVariant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
| PVar of loc * tevar
| PAnnot of loc * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of loc
| PTuple of loc * ('a,'b) pattern list
| PVariant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
type nominal_term =
(tyvar, tyvar) term
@ -98,8 +127,8 @@ type debruijn_term =
(* Constructors. *)
val ftyabs: 'b list -> ('a, 'b) term -> ('a, 'b) term
val ftyapp: ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
val ftyabs: loc:loc -> 'b list -> ('a, 'b) term -> ('a, 'b) term
val ftyapp: loc:loc -> ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
(* -------------------------------------------------------------------------- *)

@ -40,26 +40,34 @@ let rec translate_type (env : (F.tyvar * P.tyvar) list) (ty : F.nominal_type) :
P.TyMu (alpha, self ((x, alpha) :: env) ty)
| F.TyConstr (constr, tys) ->
P.TyConstr (constr, List.map (self env) tys)
| F.TyEq (ty1, ty2) ->
P.TyEq (self env ty1, self env ty2)
let print_type ty =
Printer.print_type (translate_type [] ty)
let rec translate_term env (t : F.nominal_term) : P.term =
let self = translate_term in
let annot env ty = (P.Flexible, [], translate_type env ty) in
match t with
| F.Var (_, x) ->
P.Var x
| F.Hole (_, ty, ts) ->
P.Hole (Some (translate_type env ty), List.map (self env) ts)
| F.Annot (_, t, ty) ->
P.Annot (self env t, (P.Flexible, [], translate_type env ty))
P.Annot (self env t, annot env ty)
| F.Abs (_, x, ty, t) ->
let annot = P.PAnnot (P.PVar x, (P.Flexible, [], translate_type env ty)) in
P.Abs (annot, self env t)
let x_annot = P.PAnnot (P.PVar x, annot env ty) in
P.Abs (x_annot, self env t)
| F.App (_, t1, t2) ->
P.App (self env t1, self env t2)
| F.Let (_, x, t, u) ->
P.Let (P.PVar x, self env t, self env u)
| F.Let (_, rec_, x, ty, t, u) ->
let rec_ = match rec_ with
| F.Recursive -> P.Recursive
| F.Non_recursive -> P.Non_recursive
in
let x_annot = P.PAnnot (P.PVar x, annot env ty) in
P.Let (rec_, x_annot, self env t, self env u)
| F.TyAbs (_, x, t) ->
let alpha = new_tyvar () in
P.TyAbs (alpha, self ((x, alpha) :: env) t)
@ -71,7 +79,7 @@ let rec translate_term env (t : F.nominal_term) : P.term =
P.Proj (i, self env t)
| F.LetProd (_, xs, t, u) ->
let pat = P.PTuple (List.map (fun x -> P.PVar x) xs) in
P.Let (pat , self env t, self env u)
P.Let (P.Non_recursive, pat, self env t, self env u)
| F.Variant (_, lbl, (tid, tys) , t) ->
P.Variant (
lbl,
@ -84,6 +92,14 @@ let rec translate_term env (t : F.nominal_term) : P.term =
self env t,
List.map (translate_branch env) brs
)
| F.Absurd (_, ty) ->
P.Absurd (translate_type env ty)
| F.Refl (_, ty) ->
P.Refl (translate_type env ty)
| F.Use (_, t, u) ->
let t' = self env t in
let u' = self env u in
P.Use (t', u')
and translate_branch env (pat, t) =
(translate_pattern env pat, translate_term env t)
@ -155,6 +171,8 @@ let rec translate_db_type (env : P.tyvar list) (ty : F.debruijn_type) : P.typ =
P.TyMu (alpha, self (alpha :: env) ty)
| F.TyConstr (constr, tys) ->
P.TyConstr (constr, List.map (self env) tys)
| F.TyEq (ty1, ty2) ->
P.TyEq (self env ty1, self env ty2)
let print_db_type ty =
Printer.print_type (translate_db_type [] ty)
@ -190,9 +208,28 @@ let print_type_error e =
str "Type error." ++
str "This type should be a universal type:" ++
print_db_type ty
| NotAnEqual ty ->
str "Type error." ++
str "This type should be an equality type:" ++
print_db_type ty
| UnboundTermVariable x ->
str "Scope error." ++
str "The variable %s is unbound." x
| UnboundTypeVariable x ->
str "Scope error." ++
str "The type variable %d is unbound." x
| TwoOccurencesOfSameVariable x ->
str "Scope error." ++
str "The variable %s is bound twice in a pattern." x
| ContextNotAbsurd ->
str "Type error." ++
str "The type equations in the typing environment are not contradictory."
| UnexpectedRecord ->
str "Type error." ++
str "A record was expected."
| DeclarationNotFound (Datatype.Type tid) ->
str "Scope error." ++
str "Unknown type declaration : %s." tid
| LabelNotFound (Datatype.Label lid) ->
str "Scope error." ++
str "Unknown variant constructor : %s." lid

@ -6,12 +6,19 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
| NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
| UnboundTypeVariable of tyvar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
| UnexpectedRecord
| DeclarationNotFound of Datatype.tyconstr_id
| LabelNotFound of Datatype.label_id
and arity_requirement = Index of int | Total of int
exception TypeError of type_error
exception TypeError of loc * type_error
(* -------------------------------------------------------------------------- *)
@ -37,58 +44,99 @@ module TermVarMap =
module N2DB =
DeBruijn.Nominal2deBruijn(TermVar)
(* We use a union-find data structure to represent equalities between rigid
variables and types. We need the ability to snapshot and rollback changes, to
undo the addition of an equality to the environment. *)
module UF = struct
include UnionFind.Make(UnionFind.StoreVector)
type 'a elem = 'a rref
end
module S =
Structure
(* We translate types into union-find graphs to check equality.
μ-types create cyclic graphs. Each vertex represents a type expression.
GADTs can add type equalities in the context and we represent
this by unifying their vertices in the union-find graph. This is
possible only when they have compatible structures (or one of the
side has no structure), otherwise the equality is inconsistent. *)
type vertex =
structure option UF.elem
and structure =
(* Corresponds to types from the source language (arrow, product, ...). *)
| SStruct of vertex S.structure
(* Represents ∀α.τ. We use De Bruijn levels, so we don't need to name
explicitly the bound variable α. *)
| SForall of vertex
(* A De Bruijn level corresponding to a ∀-bound variable. Using levels
instead of indices makes the equality test easier. *)
| SForallLevel of int
(* The global store of the union-find. *)
type uf_store = structure option UF.store
(* A mapping from rigid variables to union-find vertices. *)
type uf_tyvars = structure option UF.elem list
(* If the type equations introduced are inconsistent, then no need for
[store] and [tyvars] *)
type equations_env =
| Equations of { store: uf_store ; tyvars: uf_tyvars }
| Inconsistent
type env = {
(* A mapping of term variables to types. *)
types: debruijn_type TermVarMap.t;
(* A translation environment of TERM variables to TYPE indices. *)
names: N2DB.env;
(* We keep trace of whether or not the typing equations is consistent *)
equations: equations_env;
}
type _datatype_env = (unit, debruijn_type) Datatype.Env.t
let empty =
{ types = TermVarMap.empty; names = N2DB.empty }
let empty = {
types = TermVarMap.empty;
names = N2DB.empty;
equations = Equations { store = UF.new_store() ; tyvars = [] };
}
let lookup { types; names } x =
try
(* Obtain the type associated with [x]. *)
let ty = TermVarMap.find x types in
let lookup ~loc { types; names; _ } x =
(* Obtain the type associated with [x]. *)
match TermVarMap.find x types with
| exception Not_found ->
raise (TypeError (loc, UnboundTermVariable x))
| ty ->
(* Find how long ago [x] was bound. *)
let w = N2DB.lookup names x in
(* Shift the type [ty] by this amount, so that it makes sense in the
current scope. *)
Type.lift w 0 ty
with Not_found ->
(* must have been raised by [TermVarMap.find] *)
raise (TypeError (UnboundTermVariable x))
let extend_with_tevar { types; names } x ty =
let extend_with_tevar { types; names; equations } x ty =
(* Map the name [x] to [ty], and record when it was bound, without
incrementing the time. *)
{ types = TermVarMap.add x ty types;
names = N2DB.slide names x }
let extend_with_tyvar { types; names } =
(* Increment the time. *)
{ types; names = N2DB.bump names }
let singleton x ty =
extend_with_tevar empty x ty
let concat env1 env2 =
let combine _ _ ty2 = Some ty2 in
{ types = TermVarMap.union combine env1.types env2.types ;
names = N2DB.concat env1.names env2.names }
let concat_disjoint env1 env2 =
let exception Conflict of TermVarMap.key in
try
let combine x _ _ =
raise (Conflict x) in
let types = TermVarMap.union combine env1.types env2.types
and names = N2DB.concat env1.names env2.names in
Ok { types; names; }
with Conflict x -> Error x
names = N2DB.slide names x;
equations; }
let extend_with_tevar_no_dup ~loc ({ types; _ } as env) x ty =
if TermVarMap.mem x types then
raise (TypeError (loc, TwoOccurencesOfSameVariable x));
extend_with_tevar env x ty
let extend_with_tyvar { types; names; equations } =
match equations with
| Inconsistent ->
{ types; names; equations }
| Equations { store; tyvars } ->
(* Create a fresh vertex for the new type variable *)
let v = UF.make store None in
(* Extend the environment of type variables *)
let tyvars = v :: tyvars in
(* Increment the time. *)
let names = N2DB.bump names in
{ types; names ; equations = Equations { store ; tyvars } }
(* -------------------------------------------------------------------------- *)
@ -101,95 +149,32 @@ let unfold ty =
| _ ->
assert false
let rec as_arrow ty =
let rec as_arrow ~loc ty =
match ty with
| TyArrow (ty1, ty2) ->
ty1, ty2
| TyMu _ ->
as_arrow (unfold ty)
as_arrow ~loc (unfold ty)
| _ ->
raise (TypeError (NotAnArrow ty))
raise (TypeError (loc, NotAnArrow ty))
let rec as_product ty =
let rec as_product ~loc ty =
match ty with
| TyProduct tys ->
tys
| TyMu _ ->
as_product (unfold ty)
as_product ~loc (unfold ty)
| _ ->
raise (TypeError (NotAProduct ty))
raise (TypeError (loc, NotAProduct ty))
let rec as_forall ty =
let rec as_forall ~loc ty =
match ty with
| TyForall ((), ty) ->
ty
| TyMu _ ->
as_forall (unfold ty)
as_forall ~loc (unfold ty)
| _ ->
raise (TypeError (NotAForall ty))
(* -------------------------------------------------------------------------- *)
(* [equal1] groups the easy cases of the type equality test. It does not
accept arguments of the form [TyMu]. It expects a self parameter [equal]
that is used to compare the children of the two root nodes. *)
let pointwise equal tys1 tys2 =
try
List.for_all2 equal tys1 tys2
with Invalid_argument _ ->
(* Catching [Invalid_argument] is bad style, but saves a couple calls
to [List.length]. A cleaner approach would be to use arrays instead
of lists. *)
false
let equal1 equal ty1 ty2 =
match ty1, ty2 with
| TyMu _, _
| _, TyMu _ ->
assert false
| TyVar x1, TyVar x2 ->
Int.equal x1 x2
| TyArrow (ty1a, ty1b), TyArrow (ty2a, ty2b) ->
equal ty1a ty2a && equal ty1b ty2b
| TyForall ((), ty1), TyForall ((), ty2) ->
equal ty1 ty2
| TyProduct tys1, TyProduct tys2 ->
pointwise equal tys1 tys2
| TyConstr (Datatype.Type tyconstr1, tys1),
TyConstr (Datatype.Type tyconstr2, tys2) ->
String.equal tyconstr1 tyconstr2 &&
pointwise equal tys1 tys2
| (TyVar _ | TyArrow _ | TyForall _ | TyProduct _ | TyConstr _),
_ ->
false
(* -------------------------------------------------------------------------- *)
(* An unsound approximation of the equality test. (Now unused.) *)
(* Comparing two [TyMu] types simply by comparing their bodies would be
correct, but incomplete: some types that are equal would be considered
different. *)
(* Naively unfolding every [TyMu] type is sound and complete, but leads to
potential non-termination. The following code avoids non-termination by
imposing a budget limit. This makes this equality test unsound: two types
may be considered equal when they are in fact different. *)
let rec equal budget ty1 ty2 =
match ty1, ty2 with
| (TyMu _ as ty1), ty2
| ty2, (TyMu _ as ty1) ->
budget = 0 || equal (budget - 1) (unfold ty1) ty2
| _, _ ->
equal1 (equal budget) ty1 ty2
let budget =
4
let _unsound_equal ty1 ty2 =
equal budget ty1 ty2
raise (TypeError (loc, NotAForall ty))
(* -------------------------------------------------------------------------- *)
@ -197,204 +182,282 @@ let _unsound_equal ty1 ty2 =
(* The System F types produced by an ML type inference algorithm cannot
contain [TyForall] under [TyMu]. In this restricted setting, deciding
type equality is relatively easy. We proceed in two layers, as follows:
- Initially, we perform a normal (structural) equality test, going
down under [TyForall] constructors if necessary. As soon as we
hit a [TyMu] constructor on either side, we switch to the lower
layer:
- In the lower layer, we know that we cannot hit a [TyForall]
constructor (if we do, we report that the types differ). We
map each type (separately) to a graph of unification variables
(where every variable has rigid structure), then we check that
the two graphs can be unified. *)
type equality is relatively easy. We map each type to a graph of
unification variables (where every variable has rigid structure),
then we check that the two graphs can be unified. *)
exception Clash =
Structure.Iter2
module S =
Structure
type vertex =
structure UnionFind.elem
and structure =
| SRigidVar of DeBruijn.index
| SStruct of vertex S.structure
let rec translate (env : vertex list) (ty : F.debruijn_type) : vertex =
match ty with
(* This function assumes no universal quantification inside a μ-type, because
it would be difficult to check type equality otherwise. The boolean
[inside_mu] tracks whether we are already under a μ quantifier. *)
let rec translate ~loc ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
: vertex
= match ty with
| TyVar x ->
(* If [x] is bound in [env], then [x] is bound by μ, and we
already have a vertex that represents it. Otherwise, [x]
is bound by , and it is regarded as a rigid variable. *)
let n = List.length env in
if x < n then
List.nth env x
else
UnionFind.make (SRigidVar (x - n))
begin
(* If the type is closed, then [x] was bound by a quantifier before and
was added to the environment. *)
try
List.nth env x
with Not_found ->
raise (TypeError (loc, UnboundTypeVariable x))
end
| TyMu ((), ty) ->
(* Extend the environment with a mapping of this μ-bound variable
to a fresh vertex. *)
let dummy : structure = SRigidVar 0 in
let v1 = UnionFind.make dummy in
let v1 = UF.make store None in
let env = v1 :: env in
(* Translate the body. *)
let v2 = translate env ty in
let v2 = translate ~loc ~inside_mu:true store env ty in
(* Unify the vertices [v1] and [v2], keeping [v2]'s structure. *)
let v = UnionFind.merge (fun _ s2 -> s2) v1 v2 in
let v = UF.merge store (fun _ s2 -> s2) v1 v2 in
v
| TyForall _ ->
(* Either we have found a ∀ under a μ, which is unexpected, or one
of the types that we are comparing has more quantifiers than
the other. Either way, we report that the types differ. *)
raise Clash
| TyForall ((), ty) ->
assert (not inside_mu);
(* Extend the environment with a mapping of this forall-bound variable
to a fresh vertex. *)
let v1 = UF.make store (Some (SForallLevel (List.length env))) in
let env = v1 :: env in
(* Translate the body. *)
let v2 = translate ~loc ~inside_mu store env ty in
UF.make store (Some (SForall v2))
| TyArrow (ty1, ty2) ->
let v1 = translate env ty1
and v2 = translate env ty2 in
UnionFind.make (SStruct (S.TyArrow (v1, v2)))
let v1 = translate ~loc ~inside_mu store env ty1
and v2 = translate ~loc ~inside_mu store env ty2 in
UF.make store (Some (SStruct (S.TyArrow (v1, v2))))
| TyProduct tys ->
let vs = translate_list env tys in
UnionFind.make (SStruct (S.TyProduct vs))
let vs = translate_list ~loc ~inside_mu store env tys in
UF.make store (Some (SStruct (S.TyProduct vs)))
| TyConstr (id, tys) ->
let vs = translate_list env tys in
UnionFind.make (SStruct (S.TyConstr (id, vs)))
let vs = translate_list ~loc ~inside_mu store env tys in
UF.make store (Some (SStruct (S.TyConstr (id, vs))))
| TyEq (ty1, ty2) ->
let v1 = translate ~loc ~inside_mu store env ty1
and v2 = translate ~loc ~inside_mu store env ty2 in
UF.make store (Some (SStruct (S.TyEq (v1, v2))))
and translate_list env tys =
List.map (translate env) tys
and translate_list ~loc ~inside_mu store env tys =
List.map (translate ~loc ~inside_mu store env) tys
let insert q v1 v2 =
Stack.push (v1, v2) q
let unify_struct q s1 s2 =
match s1, s2 with
| SRigidVar x1, SRigidVar x2 ->
| SForallLevel x1, SForallLevel x2 ->
if x1 <> x2 then raise Clash
| SStruct s1, SStruct s2 ->
Structure.iter2 (insert q) s1 s2
| SRigidVar _, SStruct _
| SStruct _, SRigidVar _ ->
| SForall s1, SForall s2 ->
insert q s1 s2
| SForallLevel _, _
| SStruct _, _
| SForall _, _ ->
raise Clash
let merge_struct q s1 s2 =
unify_struct q s1 s2;
s1
let rec unify q (v1 : vertex) (v2 : vertex) =
let (_ : vertex) = UnionFind.merge (merge_struct q) v1 v2 in
unify_pending q
and unify_pending q =
(* We need two operations on equalities between types:
- add an equality to the equations in the environment
- check if a given equality holds modulo the equations in the environment *)
(* Both operations can be described as first decomposing a given equality
"ty1 = ty2" into "simple equalities" between a rigid variable and a type.
In fact, the union-find data structure that we use to represent an
environment of equations store exactly those simple equalities. *)
(* Then:
- to add an equality, we modify our environment by unifying the type
variables with the equated type
- to check an equality, we check that the simple equalities are already
valid in the equations of the environment, and fail otherwise *)
(* The decomposition process does not produce simple equalities if the
provided equality is absurd ("int * int = int * bool").
Then:
- if we are adding this equality to the environment, we record that the
environment is now Inconsistent
- if we are checking the equality (in a consistent environment), we fail *)
(* The functions below implement a unification procedure that implements both
these operations, depending on a [mode] parameter:
- in [Input] mode, they add an equality to the environment
- in [Check] mode, they check that the equality holds modulo the equations
in the environment *)
type mode = Input | Check
let merge_struct mode q so1 so2 : structure option =
match so1, so2 with
| Some s1, Some s2 ->
unify_struct q s1 s2;
so1
| None, so | so, None ->
match mode with
| Input ->
so
| Check ->
raise Clash
let rec unify mode store q (v1 : vertex) (v2 : vertex) =
let (_ : vertex) = UF.merge store (merge_struct mode q) v1 v2 in
unify_pending mode store q
and unify_pending mode store q =
match Stack.pop q with
| v1, v2 ->
unify q v1 v2
unify mode store q v1 v2
| exception Stack.Empty ->
()
let unify v1 v2 =
let unify mode store v1 v2 =
let q = Stack.create() in
unify q v1 v2
let rec equal ty1 ty2 =
match ty1, ty2 with
| (TyMu _ as ty1), ty2
| ty2, (TyMu _ as ty1) ->
(* We have hit a μ binder on one side. Switch to layer-1 mode. *)
begin try
let env = [] in
let v1 = translate env ty1
and v2 = translate env ty2 in
unify v1 v2;
true
with Clash ->
false
end
| _, _ ->
(* Otherwise, continue in layer-2 mode. *)
equal1 equal ty1 ty2
unify mode store q v1 v2
let unify_types ~loc mode env ty1 ty2 =
match env.equations with
| Inconsistent ->
true
| Equations { store ; tyvars } ->
try
let v1 = translate ~loc ~inside_mu:false store tyvars ty1
and v2 = translate ~loc ~inside_mu:false store tyvars ty2 in
unify mode store v1 v2;
true
with Clash ->
false
(* -------------------------------------------------------------------------- *)
(* Re-package the type equality test as a type equality check. *)
(* Re-package the type unification as a type equality check. *)
let enforce_equal ~loc env ty1 ty2 : unit =
if not (unify_types ~loc Check env ty1 ty2) then
raise (TypeError (loc, TypeMismatch (ty1, ty2)))
let (--) ty1 ty2 : unit =
if not (equal ty1 ty2) then
raise (TypeError (TypeMismatch (ty1, ty2)))
(* Re-package the type unification as an addition in the environment. *)
let add_equation ~loc env ty1 ty2 : env =
if unify_types ~loc Input env ty1 ty2 then
env
else
{ env with equations = Inconsistent }
let copy_env env store tyvars =
let store_copy = UF.copy store in
let equations = Equations { store = store_copy; tyvars } in
{ env with equations }
(* -------------------------------------------------------------------------- *)
(* The type-checker. *)
let nth_type ty tys i =
let nth_type ~loc ty tys i =
if i < 0 || i >= List.length tys then
raise (TypeError (ArityMismatch (Index i, ty)))
raise (TypeError (loc, ArityMismatch (Index i, ty)))
else
List.nth tys i
let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
let typeof = typeof datatype_env in
match t with
| Var (_, x) ->
lookup env x
| Var (loc, x) ->
lookup ~loc env x
| Hole (_, ty, ts) ->
let on_subterm t =
ignore (typeof env t) in
List.iter on_subterm ts;
ty
| Annot (_, t, ty) ->
typeof env t -- ty;
| Annot (loc, t, ty) ->
enforce_equal ~loc env (typeof env t) ty;
ty
| Abs (_, x, ty1, t) ->
let ty2 = typeof (extend_with_tevar env x ty1) t in
TyArrow (ty1, ty2)
| App (_, t, u) ->
let ty1, ty2 = as_arrow (typeof env t) in
typeof env u -- ty1;
| App (loc, t, u) ->
let ty1, ty2 = as_arrow ~loc (typeof env t) in
enforce_equal ~loc env (typeof env u) ty1;
ty2
| Let (_, x, t, u) ->
let env = extend_with_tevar env x (typeof env t) in
typeof env u
| Let (loc, rec_, x, ty, t, u) ->
let env_with_x = extend_with_tevar env x ty in
let def_env = match rec_ with
| Non_recursive -> env
| Recursive -> env_with_x
in
enforce_equal ~loc def_env (typeof def_env t) ty;
typeof env_with_x u
| TyAbs (_, (), t) ->
TyForall ((), typeof (extend_with_tyvar env) t)
| TyApp (_, t, ty2) ->
Type.subst ty2 0 (as_forall (typeof env t))
| TyApp (loc, t, ty2) ->
Type.subst ty2 0 (as_forall ~loc (typeof env t))
| Tuple (_, ts) ->
let tys = List.map (typeof env) ts in
TyProduct tys
| Proj (_, i, t) ->
| Proj (loc, i, t) ->
let ty = typeof env t in
let tys = as_product ty in
nth_type ty tys i
| Variant (_, lbl, dty, t) ->
let arg_type = typeof_variant datatype_env lbl dty in
let tys = as_product ~loc ty in
nth_type ~loc ty tys i
| Variant (loc, lbl, dty, t) ->
let arg_type = typeof_variant datatype_env ~loc lbl dty in
let ty = typeof env t in
ty -- arg_type;
enforce_equal ~loc env ty arg_type