diff --git a/test/Test_MakeTerm.re b/test/Test_MakeTerm.re index 2a503d64d..13894ee3b 100644 --- a/test/Test_MakeTerm.re +++ b/test/Test_MakeTerm.re @@ -20,26 +20,57 @@ let tests = [ Cast( Var("x") |> Pat.fresh, Parens( - TupLabel(Label("l") |> Typ.fresh, String |> Typ.fresh) // TODO Do we want to wrap the singleton case in a product + Prod([ + TupLabel(Label("l") |> Typ.fresh, String |> Typ.fresh) + |> Typ.fresh, + ]) |> Typ.fresh, ) |> Typ.fresh, Unknown(Internal) |> Typ.fresh, ) |> Pat.fresh, - Parens(String("a") |> Exp.fresh) |> Exp.fresh, // TODO Should we require parens around singleton tables to ascribe labels + Parens(String("a") |> Exp.fresh) |> Exp.fresh, Var("x") |> Exp.fresh, ) |> Exp.fresh, - "let x : (l=String) = \"a\" in x", + "let x : (l=String) = (\"a\") in x", ) }), - test_case("", `Quick, () => { + test_case("Assigning labeled tuple to variable", `Quick, () => { exp_check( - Int(7) |> Exp.fresh, + Let( + Var("x") |> Pat.fresh, + Parens( + Tuple([ + TupLabel(Label("l") |> Exp.fresh, Int(32) |> Exp.fresh) + |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + Let( + Cast( + Var("y") |> Pat.fresh, + Parens( + Prod([ + TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh) + |> Typ.fresh, + ]) + |> Typ.fresh, + ) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Pat.fresh, + Var("x") |> Exp.fresh, + Var("y") |> Exp.fresh, + ) + |> Exp.fresh, + ) + |> Exp.fresh, "let x = (l=32) in -let y : (l=Int) = x in - ", + let y : (l=Int) = x in y", ) }), ]; diff --git a/test/Test_Statics.re b/test/Test_Statics.re index 0d8b6b953..bca2aea3d 100644 --- a/test/Test_Statics.re +++ b/test/Test_Statics.re @@ -273,4 +273,80 @@ let tests = ), unlabeled_tuple_to_labeled_fails, simple_inconsistency, + test_case("Assigning labeled tuple to variable", `Quick, () => { + alco_check( + "let x = (l=32) in + let y : (l=Int) = x in y", + Some( + Prod([ + TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh) |> Typ.fresh, + ]) + |> Typ.fresh, + ), + type_of( + Let( + Var("x") |> Pat.fresh, + Parens( + Tuple([ + TupLabel(Label("l") |> Exp.fresh, Int(32) |> Exp.fresh) + |> Exp.fresh, + ]) + |> Exp.fresh, + ) + |> Exp.fresh, + Let( + Cast( + Var("y") |> Pat.fresh, + Parens( + Prod([ + TupLabel(Label("l") |> Typ.fresh, Int |> Typ.fresh) + |> Typ.fresh, + ]) + |> Typ.fresh, + ) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Pat.fresh, + Var("x") |> Exp.fresh, + Var("y") |> Exp.fresh, + ) + |> Exp.fresh, + ) + |> Exp.fresh, + ), + ) + }), + test_case("Singleton Labled Tuple ascription in let", `Quick, () => { + alco_check( + "let x : (l=String) = (\"a\") in x", + Some( + Prod([ + TupLabel(Label("l") |> Typ.fresh, String |> Typ.fresh) + |> Typ.fresh, + ]) + |> Typ.fresh, + ), + type_of( + Let( + Cast( + Var("x") |> Pat.fresh, + Parens( + Prod([ + TupLabel(Label("l") |> Typ.fresh, String |> Typ.fresh) + |> Typ.fresh, + ]) + |> Typ.fresh, + ) + |> Typ.fresh, + Unknown(Internal) |> Typ.fresh, + ) + |> Pat.fresh, + Parens(String("a") |> Exp.fresh) |> Exp.fresh, // TODO Need to assert there's no inconsistency in this branch + Var("x") |> Exp.fresh, + ) + |> Exp.fresh, + ), + ) + }), ];