diff --git a/prelude.alc b/prelude.alc index 0d40395..dc9d911 100644 --- a/prelude.alc +++ b/prelude.alc @@ -11,13 +11,6 @@ let universe = type_(9, 1) lambda (x : T) wrap T x -let foo = debug-track - lambda_implicit (a : type) - lambda_implicit (b : type) - lambda (c : a, d : b) - c -let test = foo(1, 2) - let implicit-wrap = lambda_curry ((T : type_(10, 0))) lambda (x : T) wrap T x @@ -153,29 +146,28 @@ let _&_ = wrapped (forall (a : U, b : U) -> (res : U)) let covariant = - debug-track - lambda_curry (U : type_(9, 1), a : U) - unwrap - intrinsic - """" - local string_array = terms_gen.declare_array(terms_gen.builtin_string) - return terms.value.closure( - "#covariant-args", - terms.typed_term.tuple_elim( - string_array("base"), - terms.typed_term.bound_variable(1), - 1, - terms.typed_term.variance_cons( - terms.typed_term.literal( - terms.value.host_value(true) - ), - terms.typed_term.bound_variable(2) - ) - ), - terms.runtime_context() - ) - : - wrapped (forall ((rel : srel(a))) -> (res : variance(a))) + lambda_curry (U : type_(9, 1), a : U) + unwrap + intrinsic + """" + local string_array = terms_gen.declare_array(terms_gen.builtin_string) + return terms.value.closure( + "#covariant-args", + terms.typed_term.tuple_elim( + string_array("base"), + terms.typed_term.bound_variable(1), + 1, + terms.typed_term.variance_cons( + terms.typed_term.literal( + terms.value.host_value(true) + ), + terms.typed_term.bound_variable(2) + ) + ), + terms.runtime_context() + ) + : + wrapped (forall ((rel : srel(a))) -> (res : variance(a))) let contravariant = lambda_curry (U : type_(9, 1), a : U) @@ -327,7 +319,7 @@ let new-host-type-family = lambda (unique-id : host-unique-id, signature : type_ signature_ : wrapped(type_(1, 0)), variance_ : wrapped(host-family-sig-variances(unwrap(signature_)))) -> - ((family : wrapped(signature))) + (family : wrapped(unwrap(signature_))) let (family) = inner(unique-id, wrap(signature), wrap(variance)) unwrap(family) let new-host-type = lambda (unique-id : host-unique-id) @@ -338,7 +330,7 @@ let new-host-type = lambda (unique-id : host-unique-id) let host-array-type = new-host-type-family new-host-unique-id("array") forall ((T : host-type)) -> (T : host-type) - tuple-of-implicit debug-track(covariant(subtyping)) + tuple-of-implicit covariant(subtyping) let host-array-new = lambda (T : host-type) let inner = intrinsic diff --git a/tests/implicit.alc b/tests/implicit.alc index 170ab93..0f6ff1d 100644 --- a/tests/implicit.alc +++ b/tests/implicit.alc @@ -2,6 +2,13 @@ let id = lambda_implicit (T : type_(10, 0)) lambda (x : T) x +let foo = + lambda_implicit (a : type) + lambda_implicit (b : type) + lambda (c : a, d : b) + c +let test = foo(1, 2) + # TODO: test this when tuple-desc can do more than just star-0 #let point = lambda_implicit (U : type_(10)) # lambda (T : U)