Repository: tweag/nickel
Pull request #664 (2022-03-18 15:31:34)

Xavier/type wildcards
@yannham Here's a draft for the wildcards :-) Let me know what you think.  I think I should add more tests, but I'm not yet sure where, and which kinds.

Implementation of #495, type wildcards.

Wildcards are implemented as a type `AbsType::Wildcard(usize)`, marked with a unique `usize` identifier.

Type checking is done by interpreting wildcards as type variables during unification.  After a term is typechecked, the type variable associated with each wildcard is converted to a concrete type, and the mapping from wildcard ID to concrete type is returned: `wildcards: HashMap<usize, Types>`.

A new program transformation `substitute_wildcards` is added.  It takes the mapping `wildcards` as input, along with a term, and substitutes any wildcard annotation in the term with its concrete type taken from `wildcards`, or with `Dyn` if no type was inferred for that particular wildcard.

The cache has been updated to store the wildcard mappings for each file after type checking is done, such that they can be reused when later applying program transformations to the same file.

xlambein: Actually, I realize I didn't take the LSP into account at all.  It won't have access to the wildcard's inferred type, I expect.  I'll look into this.
xlambein: > I initially thought about generating all the free variables required at once (for example, when converting types to typewrappers)

That's what I did at first, but it required more changes to the codebase, and I felt less confident about the implementation.

> However, the current PR doesn't seem to work well with composed types:

Ah, indeed!  Thanks, I'll use `traverse` to fix this :-)
yannham: Another shower thought, that lead to the unveiling of another issue.

Until now, one nice thing about typed block is that the obligation of writing a type annotation on them make typechecking modular. This means that, thinking about the refactoring that is currently in the working, we can:

1. Allocate a new unification table for each typed block, and drop it all at once in the end. We don't need to remember unification variable spanned inside a block, because they can't escape the block.
2. We don't right now, but if we want to implement some parallelism, we can typecheck typed block in parallel, because all they need is a read-only access to the ast, but don't need to care about type inference within a block.

I thus wonder what we should do about

```nickel
let f : _ -> _ = fun x = x + 1 in
let g : Num = f 0
```

With wildcard, if we want to actually give the right type to `f`, we have to wait for it to have been fully typechecked, before we can typecheck `g`, which breaks modularity. One solution would be that any wildcard appears as `Dyn` from the outside of the typed block, which rejects more programs (like this one) but preserve the "I can know the type of a typed block just by poking at the top-level AST node" property.

I wondered, how the current PR handled that, and it turns out it does something that is unsound:

```nickel
nickel> let f : _ -> _ = fun x => x + 1
nickel> let g : Str = f "a"
nickel> g
error: type error
  ┌─ repl-input-2:1:27
  │
1 │ let f : _ -> _ = fun x => x + 1
  │                           ^ this expression has type Str, but Num was expected
  │
  ┌─ repl-input-3:1:17
  │
1 │ let g : Str = f "a"
  │                 --- evaluated to this
  │
  = +, 1st argument
```

It accepts `g`, while it should surely reject it (as the dynamic type error show). I think there is an issue with `apparent_type`. Why exactly did you want to exclude the case of wildcards?
yannham: ```
nickel> let f : _ -> _ = fun x => x + 1
nickel> let g : Str = f "a"
nickel> g
error: contract broken by the caller
  ┌─ :1:1
  │
1 │ Num -> Num
  │ --- expected type of the argument provided by the caller
  │
...etc
```

Beware that this is probably not the behavior we want. Blame safety is an important property enjoyed by the type system (although it hasn't been formally proved, the type system not being formalized yet, but its most probably the case). It is illustrated by the slogan "well typed program can't be blamed": typing should be always more restrictive than contracts, and an expression that typechecks should never cause contract violation at runtime.

Here, this case is broken. I think there are different acceptable behaviors for this example:

1. The occurrence of `f` inside `g` is given the type `Num -> Num`. Put differently, the apparent type of `f` is `Num -> Num`. This breaks the modularity of typechecking, but could still be a reasonable design decision. It gives `f` its actual, most precise type.
2. Just assign `Dyn` to the apparent type of `f`. This ensures that we can't use it in typed code without further casts, and force the user to write explicit annotations if they want to use it somewhere else. It is forward-compatible with 1.

I think what you do is still to give the apparent type of `f` `_a -> _b`, for some unification variables `_a` and `_b` unrelated to the one used in the typechecking of `f`.

My previous suggestion, that the occurrence of `f` inside `g` is given the type `Dyn -> Dyn`, is unfortunately unsound too. Indeed, `Num -> Num` is not a subtype of `Dyn -> Dyn`, and if currently it is harder to break, it is very possible that in the future the typechecker will accept something of type `Str` where something of type `Dyn`. This would make this example typecheck again.

Right now, I would tend to think that 2. is probably is easiest way forward. It is a bit restrictive, but I expect wildcards to be used mainly as a way of calling the typechecker to the rescue for a block, not as a signature for a function or a value that is expected to be reused elsewhere in typed code. What's more, if we were wrong, we can always switch to 1: strictly more programs will typecheck.
xlambein: Finally got some time to get back into this.  I gave a quick shot at (2).  Do you think setting the apparent type to `Dyn` for any type containing a wildcard is enough?  E.g.:

```rust
match t {
    Term::MetaValue(MetaValue {
        types: Some(Contract { types: ty, .. }),
        ..
    }) => ApparentType::Annotated(Types(if ty.0.is_wildcard() {
        AbsType::Dyn()
    } else {
        ty.0.clone()
            .try_map(|ty| if ty.0.is_wildcard() { Err(()) } else { Ok(ty) })
            .unwrap_or(AbsType::Dyn())
    })),
    // ...
}
```
xlambein: Actually, I can do better and just revert to the default behavior without the wildcard:

```rust
match t {
    Term::MetaValue(MetaValue {
        types: Some(Contract { types: ty, .. }),
        value,
        ..
    }) => {
        // Check whether the type is a wildcard
        let mut has_wildcard = false;
        let ty = ty
            .clone()
            .traverse::<_, _, std::convert::Infallible>(
                &mut |ty, has_wildcard| {
                    if ty.0.is_wildcard() {
                        *has_wildcard = true;
                    }
                    Ok(ty)
                },
                &mut has_wildcard,
                TraverseOrder::TopDown,
            )
            .unwrap();
        if has_wildcard {
            // There's a wildcard => Use the apparent type of the inner value, or Dyn
            if let Some(value) = value {
                apparent_type(value.as_ref(), envs, resolver)
            } else {
                ApparentType::Annotated(Types(AbsType::Dyn()))
            }
        } else {
            // No wildcard => Use the type annotation
            ApparentType::Annotated(ty)
        }
    }
    // ...
}
```
yannham: @xlambein do you think you can take a look at this PR soon? This has been open for a while, and also approved for quite some time. Some of the comments are open remarks, but need not be done in this PR (like the derive traversal using a macro). Answering to the others shouldn't be very long. I'm asking because I've started refactoring the typechecker a bit, but I need this to be amended if needed and merged to avoid too much conflict pain.
yannham: No worries, it's just that I think we should keep the discussion focused here as much as possible rather than on multiple side channels, because here  it is public, accessible and persistent, and otherwise it's hard to know when we come back at a PR what is the next action to take and whose responsibility it is (if I don't see any answer to my comments I assume have nothing to do :slightly_smiling_face: )

Patch:
diff --git a/src/cache.rs b/src/cache.rs
index fcbcc34b..abac08a3 100644
--- a/src/cache.rs
+++ b/src/cache.rs
@@ -6,7 +6,7 @@ use crate::position::TermPos;
 use crate::stdlib as nickel_stdlib;
 use crate::term::{RichTerm, SharedTerm, Term};
 use crate::transform::import_resolution;
-use crate::typecheck;
+use crate::typecheck::{self, TypeCheckingOutput, Wildcards};
 use crate::typecheck::{linearization::StubHost, type_check};
 use crate::types::UnboundTypeVariableError;
 use crate::{eval, parser, transform};
@@ -68,6 +68,8 @@ pub struct Cache {
     terms: HashMap<FileId, CachedTerm>,
     /// The list of ids corresponding to the stdlib modules
     stdlib_ids: Option<Vec<FileId>>,
+    /// The inferred type of wildcards for each `FileId`.
+    wildcards: HashMap<FileId, Wildcards>,
 
     #[cfg(debug_assertions)]
     /// Skip loading the stdlib, used for debugging purpose
@@ -205,6 +207,7 @@ impl Cache {
             files: Files::new(),
             file_ids: HashMap::new(),
             terms: HashMap::new(),
+            wildcards: HashMap::new(),
             imports: HashMap::new(),
             stdlib_ids: None,
 
@@ -437,8 +440,10 @@ impl Cache {
             }
             Some(CachedTerm { term, state, .. }) if *state >= EntryState::Parsed => {
                 if *state < EntryState::Typechecking {
-                    type_check(term, global_env, self, StubHost::<(), (), _>::new())?;
+                    let (TypeCheckingOutput { wildcards, .. }, _) =
+                        type_check(term, global_env, self, StubHost::<(), (), _>::new())?;
                     self.update_state(file_id, EntryState::Typechecking);
+                    self.wildcards.insert(file_id, wildcards);
                 }
 
                 if let Some(imports) = self.imports.get(&file_id).cloned() {
@@ -469,7 +474,7 @@ impl Cache {
                     let CachedTerm {
                         term, parse_errs, ..
                     } = self.terms.remove(&file_id).unwrap();
-                    let term = transform::transform(term)?;
+                    let term = transform::transform(term, self.wildcards.get(&file_id))?;
                     self.terms.insert(
                         file_id,
                         CachedTerm {
@@ -520,6 +525,7 @@ impl Cache {
                     state,
                     parse_errs,
                 } = self.terms.remove(&file_id).unwrap();
+                let wildcards = self.wildcards.get(&file_id);
 
                 if state < EntryState::Transforming {
                     let pos = term.pos;
@@ -528,7 +534,7 @@ impl Cache {
                         Term::Record(ref mut map, _) => {
                             let map_res: Result<_, UnboundTypeVariableError> = std::mem::take(map)
                                 .into_iter()
-                                .map(|(id, t)| Ok((id, transform::transform(t)?)))
+                                .map(|(id, t)| Ok((id, transform::transform(t, wildcards)?)))
                                 .collect();
                             *map = map_res.map_err(|err| {
                                 CacheError::Error(ImportError::ParseErrors(err.into(), pos))
@@ -537,14 +543,17 @@ impl Cache {
                         Term::RecRecord(ref mut map, ref mut dyn_fields, ..) => {
                             let map_res: Result<_, UnboundTypeVariableError> = std::mem::take(map)
                                 .into_iter()
-                                .map(|(id, t)| Ok((id, transform::transform(t)?)))
+                                .map(|(id, t)| Ok((id, transform::transform(t, wildcards)?)))
                                 .collect();
 
                             let dyn_fields_res: Result<_, UnboundTypeVariableError> =
                                 std::mem::take(dyn_fields)
                                     .into_iter()
                                     .map(|(id_t, t)| {
-                                        Ok((transform::transform(id_t)?, transform::transform(t)?))
+                                        Ok((
+                                            transform::transform(id_t, wildcards)?,
+                                            transform::transform(t, wildcards)?,
+                                        ))
                                     })
                                     .collect();
 
@@ -689,8 +698,10 @@ impl Cache {
             return Err(Error::ParseErrors(errs));
         }
         let (term, pending) = import_resolution::resolve_imports(term, self)?;
-        type_check(&term, global_env, self, StubHost::<(), (), _>::new())?;
-        let term = transform::transform(term).map_err(|err| Error::ParseErrors(err.into()))?;
+        let (TypeCheckingOutput { wildcards, .. }, _) =
+            type_check(&term, global_env, self, StubHost::<(), (), _>::new())?;
+        let term = transform::transform(term, Some(&wildcards))
+            .map_err(|err| Error::ParseErrors(err.into()))?;
         Ok((term, pending))
     }
 
diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 2e2cd478..16093a2c 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -66,7 +66,11 @@ use crate::{
     label::Label,
 };
 
-grammar<'input, 'err>(src_id: FileId, errors: &'err mut Vec<ErrorRecovery<usize, Token<'input>, ParseError>>);
+grammar<'input, 'err, 'wcard>(
+    src_id: FileId,
+    errors: &'err mut Vec<ErrorRecovery<usize, Token<'input>, ParseError>>,
+    next_wildcard_id: &'wcard mut usize,
+);
 
 WithPos<Rule>: Rule = <l: @L> <t: Rule> <r: @R> => t.with_pos(mk_pos(src_id, l, r));
 
@@ -762,6 +766,11 @@ TypeAtom: Types = {
         Types(AbsType::Enum(Box::new(ty)))
     },
     "{" "_" ":" <Types> "}" => Types(AbsType::DynRecord(Box::new(<>))),
+    "_" => {
+        let id = *next_wildcard_id;
+        *next_wildcard_id += 1;
+        Types(AbsType::Wildcard(id))
+    },
 }
 
 extern {
diff --git a/src/parser/mod.rs b/src/parser/mod.rs
index f8a0e085..7483a48e 100644
--- a/src/parser/mod.rs
+++ b/src/parser/mod.rs
@@ -37,8 +37,9 @@ impl grammar::ExtendedTermParser {
         lexer: lexer::Lexer,
     ) -> Result<(ExtendedTerm, ParseErrors), ParseError> {
         let mut parse_errors = Vec::new();
+        let mut next_wildcard_id = 0;
         let result = self
-            .parse(file_id, &mut parse_errors, lexer)
+            .parse(file_id, &mut parse_errors, &mut next_wildcard_id, lexer)
             .map_err(|err| ParseError::from_lalrpop(err, file_id));
 
         let parse_errors = ParseErrors::from_recoverable(parse_errors, file_id);
@@ -71,8 +72,9 @@ impl grammar::TermParser {
         lexer: lexer::Lexer,
     ) -> Result<(RichTerm, ParseErrors), ParseError> {
         let mut parse_errors = Vec::new();
+        let mut wildcard_id = 0;
         let result = self
-            .parse(file_id, &mut parse_errors, lexer)
+            .parse(file_id, &mut parse_errors, &mut wildcard_id, lexer)
             .map_err(|err| ParseError::from_lalrpop(err, file_id));
 
         let parse_errors = ParseErrors::from_recoverable(parse_errors, file_id);
diff --git a/src/parser/uniterm.rs b/src/parser/uniterm.rs
index e09d9951..7e5c4f0a 100644
--- a/src/parser/uniterm.rs
+++ b/src/parser/uniterm.rs
@@ -352,7 +352,8 @@ pub fn fix_type_vars(ty: &mut Types) {
             | AbsType::Str()
             | AbsType::Sym()
             | AbsType::Flat(_)
-            | AbsType::RowEmpty() => (),
+            | AbsType::RowEmpty()
+            | AbsType::Wildcard(_) => (),
             AbsType::Arrow(ref mut s, ref mut t) => {
                 fix_type_vars_aux(s.as_mut(), Cow::Borrowed(bound_vars.as_ref()));
                 fix_type_vars_aux(t.as_mut(), bound_vars);
diff --git a/src/pretty.rs b/src/pretty.rs
index db252420..176d24c4 100644
--- a/src/pretty.rs
+++ b/src/pretty.rs
@@ -782,6 +782,7 @@ where
                     .append(allocator.space())
                     .append(codom.pretty(allocator)),
             },
+            Wildcard(_) => allocator.text("_"),
         }
     }
 }
diff --git a/src/program.rs b/src/program.rs
index 81173f68..652736ae 100644
--- a/src/program.rs
+++ b/src/program.rs
@@ -150,7 +150,7 @@ impl Program {
 
         let rt = cache.parse_nocache(*main_id)?.0;
         let rt = if apply_transforms {
-            crate::transform::transform(rt).unwrap()
+            crate::transform::transform(rt, None).unwrap()
         } else {
             rt
         };
diff --git a/src/repl/mod.rs b/src/repl/mod.rs
index 12d2aa6e..49522d35 100644
--- a/src/repl/mod.rs
+++ b/src/repl/mod.rs
@@ -12,6 +12,7 @@ use crate::identifier::Ident;
 use crate::parser::{grammar, lexer, ExtendedTerm};
 use crate::term::{RichTerm, Term};
 use crate::transform::import_resolution;
+use crate::typecheck::TypeCheckingOutput;
 use crate::types::Types;
 use crate::{eval, transform, typecheck};
 use codespan::FileId;
@@ -134,7 +135,8 @@ impl ReplImpl {
                 repl_impl.cache.resolve_imports(*id).unwrap();
             }
 
-            typecheck::type_check_in_env(&t, &repl_impl.env.type_env, &repl_impl.cache)?;
+            let TypeCheckingOutput { wildcards, .. } =
+                typecheck::type_check_in_env(&t, &repl_impl.env.type_env, &repl_impl.cache)?;
 
             if let Some(id) = id {
                 typecheck::Envs::env_add(
@@ -154,7 +156,8 @@ impl ReplImpl {
                     })?;
             }
 
-            let t = transform::transform(t).map_err(|err| Error::ParseErrors(err.into()))?;
+            let t = transform::transform(t, Some(&wildcards))
+                .map_err(|err| Error::ParseErrors(err.into()))?;
             for id in &pending {
                 repl_impl
                     .cache
@@ -230,7 +233,21 @@ impl Repl for ReplImpl {
         for id in &pending {
             self.cache.resolve_imports(*id).unwrap();
         }
-        typecheck::type_check_in_env(&term, &self.env.type_env, &self.cache)?;
+        let TypeCheckingOutput { wildcards, .. } =
+            typecheck::type_check_in_env(&term, &self.env.type_env, &self.cache)?;
+        // Substitute the wildcard types for their inferred types
+        // We need to `traverse` the term, in case the type depends on inner terms that also contain wildcards
+        let term = term
+            .traverse(
+                &mut |rt: RichTerm, _| -> Result<RichTerm, std::convert::Infallible> {
+                    Ok(transform::substitute_wildcards::transform_one(
+                        rt, &wildcards,
+                    ))
+                },
+                &mut (),
+                crate::term::TraverseOrder::TopDown,
+            )
+            .unwrap();
 
         Ok(typecheck::apparent_type(
             term.as_ref(),
diff --git a/src/transform/free_vars.rs b/src/transform/free_vars.rs
index 1a69031f..99bd9d94 100644
--- a/src/transform/free_vars.rs
+++ b/src/transform/free_vars.rs
@@ -178,7 +178,8 @@ fn collect_type_free_vars(ty: &mut Types, set: &mut HashSet<Ident>) {
         | AbsType::Str()
         | AbsType::Sym()
         | AbsType::Var(_)
-        | AbsType::RowEmpty() => (),
+        | AbsType::RowEmpty()
+        | AbsType::Wildcard(_) => (),
         AbsType::Forall(_, ty)
         | AbsType::Enum(ty)
         | AbsType::StaticRecord(ty)
diff --git a/src/transform/mod.rs b/src/transform/mod.rs
index bc3c3fad..0e5e90ef 100644
--- a/src/transform/mod.rs
+++ b/src/transform/mod.rs
@@ -4,6 +4,7 @@ use crate::{
     eval::{lazy::Thunk, Closure, Environment, IdentKind},
     identifier::Ident,
     term::{Contract, RichTerm, Term, TraverseOrder},
+    typecheck::Wildcards,
     types::{AbsType, Types, UnboundTypeVariableError},
 };
 
@@ -16,6 +17,7 @@ pub mod desugar_destructuring;
 pub mod free_vars;
 pub mod import_resolution;
 pub mod share_normal_form;
+pub mod substitute_wildcards;
 
 /// Apply all program transformations, excepted import resolution that is currently performed
 /// earlier, as it needs to be done before typechecking.
@@ -23,15 +25,25 @@ pub mod share_normal_form;
 /// Do not perform transformations on the imported files. If needed, either do it yourself using
 /// pending imports returned by [`resolve_imports`][import_resolution::resolve_imports] or use the
 /// [cache][crate::cache::Cache].
-pub fn transform(mut rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
+pub fn transform(
+    mut rt: RichTerm,
+    wildcards: Option<&Wildcards>,
+) -> Result<RichTerm, UnboundTypeVariableError> {
     free_vars::transform(&mut rt);
-    transform_no_free_vars(rt)
+    transform_no_free_vars(rt, wildcards)
 }
 
 /// Same as [`transform`], but doesn't apply the free vars transformation.
-pub fn transform_no_free_vars(rt: RichTerm) -> Result<RichTerm, UnboundTypeVariableError> {
+pub fn transform_no_free_vars(
+    rt: RichTerm,
+    wildcards: Option<&Wildcards>,
+) -> Result<RichTerm, UnboundTypeVariableError> {
     let rt = rt.traverse(
-        &mut |rt: RichTerm, _| -> Result<RichTerm, UnboundTypeVariableError> {
+        &mut |mut rt: RichTerm, _| -> Result<RichTerm, UnboundTypeVariableError> {
+            // Start by substituting any wildcard with its inferred type
+            if let Some(wildcards) = wildcards {
+                rt = substitute_wildcards::transform_one(rt, wildcards);
+            }
             // before anything, we have to desugar the syntax
             let rt = desugar_destructuring::transform_one(rt);
             // We need to do contract generation before wrapping stuff in variables
diff --git a/src/transform/substitute_wildcards.rs b/src/transform/substitute_wildcards.rs
new file mode 100644
index 00000000..9a3eb82b
--- /dev/null
+++ b/src/transform/substitute_wildcards.rs
@@ -0,0 +1,65 @@
+//! Substitute wildcard types with their inferred type.
+//!
+//! During type checking, wildcard types are treated as type variables that may end up unified
+//! with a concrete type.  If this is the case, this pass will substitute these wildcards with
+//! the type inferred during type checking.  Otherwise, wildcards will be substituted with
+//! `Dyn`.
+use std::{convert::Infallible, rc::Rc};
+
+use crate::{
+    label::Label,
+    match_sharedterm,
+    term::{Contract, MetaValue, RichTerm, Term, TraverseOrder},
+    typecheck::Wildcards,
+    types::{AbsType, Types},
+};
+
+/// If the top-level node of the AST is a meta-value with a wildcard type annotation, replace
+/// both the type annotation and the label's type with the inferred type.
+pub fn transform_one(rt: RichTerm, wildcards: &Wildcards) -> RichTerm {
+    let pos = rt.pos;
+    match_sharedterm! {rt.term,
+        with {
+            Term::MetaValue(meta @ MetaValue {
+                types: Some(_),
+                ..
+            }) => {
+                let mut meta = meta;
+                let Contract { types, label } = meta.types.take().unwrap();  // Safe, we know there's a type
+
+                // Replace the type annotation and the blame label
+                let types = substitute_wildcards_recursively(types, wildcards);
+                let label_types = substitute_wildcards_recursively(label.types.as_ref().clone(), wildcards);
+
+                let label = Label {
+                    types: Rc::new(label_types),
+                    ..label
+                };
+                meta.types = Some(Contract { types, label });
+
+                RichTerm::new(Term::MetaValue(meta), pos)
+            }
+        } else rt
+    }
+}
+
+/// Get the inferred type for a wildcard, or Dyn if no type was inferred.
+fn get_wildcard_type(wildcards: &Wildcards, id: usize) -> Types {
+    wildcards.get(id).cloned().unwrap_or(Types(AbsType::Dyn()))
+}
+
+/// Recursively substitutes wildcards for their inferred type inside a given type.
+fn substitute_wildcards_recursively(ty: Types, wildcards: &Wildcards) -> Types {
+    ty.traverse::<_, _, Infallible>(
+        &mut |ty, _| {
+            if let Types(AbsType::Wildcard(id)) = ty {
+                Ok(get_wildcard_type(wildcards, id))
+            } else {
+                Ok(ty)
+            }
+        },
+        &mut (),
+        TraverseOrder::TopDown,
+    )
+    .unwrap()
+}
diff --git a/src/typecheck/mod.rs b/src/typecheck/mod.rs
index 7b184bc8..584341f0 100644
--- a/src/typecheck/mod.rs
+++ b/src/typecheck/mod.rs
@@ -44,7 +44,7 @@ use crate::cache::ImportResolver;
 use crate::environment::Environment as GenericEnvironment;
 use crate::error::TypecheckError;
 use crate::identifier::Ident;
-use crate::term::{Contract, MetaValue, RichTerm, StrChunk, Term};
+use crate::term::{Contract, MetaValue, RichTerm, StrChunk, Term, TraverseOrder};
 use crate::types::{AbsType, Types};
 use crate::{mk_tyw_arrow, mk_tyw_enum, mk_tyw_enum_row, mk_tyw_record, mk_tyw_row};
 use std::collections::{HashMap, HashSet};
@@ -65,6 +65,9 @@ use operation::{get_bop_type, get_nop_type, get_uop_type};
 /// The typing environment.
 pub type Environment = GenericEnvironment<Ident, TypeWrapper>;
 
+/// Mapping from wildcard ID to inferred type
+pub type Wildcards = Vec<Types>;
+
 /// A structure holding the two typing environments, the global and the local.
 ///
 /// The global typing environment is constructed from the global term environment (see
@@ -175,6 +178,16 @@ pub struct State<'a> {
     ///
     /// Used for error reporting.
     names: &'a mut HashMap<usize, Ident>,
+    /// A mapping from wildcard ID to unification variable.
+    wildcard_vars: &'a mut Vec<TypeWrapper>,
+}
+
+/// The result of type checking a term.
+pub struct TypeCheckingOutput {
+    /// Inferred type of the term.
+    pub types: Types,
+    /// Inferred types of wildcards within the term.
+    pub wildcards: Wildcards,
 }
 
 /// Typecheck a term.
@@ -189,13 +202,14 @@ pub fn type_check<LL>(
     global_env: &Environment,
     resolver: &impl ImportResolver,
     mut linearizer: LL,
-) -> Result<(Types, LL::Completed), TypecheckError>
+) -> Result<(TypeCheckingOutput, LL::Completed), TypecheckError>
 where
     LL: Linearizer<CompletionExtra = (UnifTable, HashMap<usize, Ident>)>,
 {
     let (mut table, mut names) = (UnifTable::new(), HashMap::new());
     let mut building = Linearization::new(LL::Building::default());
     let ty = table.fresh_unif_var();
+    let mut wildcard_vars = vec![];
 
     {
         let mut state: State = State {
@@ -203,6 +217,7 @@ where
             table: &mut table,
             constr: &mut RowConstr::new(),
             names: &mut names,
+            wildcard_vars: &mut wildcard_vars,
         };
 
         type_check_(
@@ -216,7 +231,10 @@ where
         )?;
     }
 
-    let result = to_type(&table, ty);
+    let result = TypeCheckingOutput {
+        types: to_type(&table, ty),
+        wildcards: wildcard_vars_to_type(wildcard_vars, &table),
+    };
     let lin = linearizer.complete(building, (table, names)).into_inner();
 
     Ok((result, lin))
@@ -236,25 +254,35 @@ pub fn type_check_in_env(
     t: &RichTerm,
     global: &Environment,
     resolver: &dyn ImportResolver,
-) -> Result<Types, TypecheckError> {
-    let mut state = State {
-        resolver,
-        table: &mut UnifTable::new(),
-        constr: &mut RowConstr::new(),
-        names: &mut HashMap::new(),
-    };
-    let ty = state.table.fresh_unif_var();
-    type_check_(
-        &mut state,
-        Envs::from_global(global),
-        &mut Linearization::new(()),
-        StubHost::<()>::new(),
-        false,
-        t,
-        ty.clone(),
-    )?;
-
-    Ok(to_type(state.table, ty))
+) -> Result<TypeCheckingOutput, TypecheckError> {
+    let mut table = UnifTable::new();
+    let ty = table.fresh_unif_var();
+    let mut wildcard_vars = vec![];
+
+    {
+        let mut state: State = State {
+            resolver,
+            table: &mut table,
+            constr: &mut RowConstr::new(),
+            names: &mut HashMap::new(),
+            wildcard_vars: &mut wildcard_vars,
+        };
+
+        type_check_(
+            &mut state,
+            Envs::from_global(global),
+            &mut Linearization::new(()),
+            StubHost::<()>::new(),
+            false,
+            t,
+            ty.clone(),
+        )?;
+    }
+
+    Ok(TypeCheckingOutput {
+        types: to_type(&table, ty),
+        wildcards: wildcard_vars_to_type(wildcard_vars, &table),
+    })
 }
 
 /// Typecheck a term against a specific type.
@@ -392,7 +420,14 @@ fn type_check_<L: Linearizer>(
                 .map_err(|err| err.into_typecheck_err(state, rt.pos))
         }
         Term::Let(x, re, rt, attrs) => {
-            let ty_let = binding_type(re.as_ref(), &envs, state.table, strict, state.resolver);
+            let ty_let = binding_type(
+                re.as_ref(),
+                &envs,
+                state.table,
+                state.wildcard_vars,
+                strict,
+                state.resolver,
+            );
             if attrs.rec {
                 envs.insert(x.clone(), ty_let.clone());
             }
@@ -414,7 +449,14 @@ fn type_check_<L: Linearizer>(
             type_check_(state, envs, lin, linearizer, strict, rt, ty)
         }
         Term::LetPattern(x, pat, re, rt) => {
-            let ty_let = binding_type(re.as_ref(), &envs, state.table, strict, state.resolver);
+            let ty_let = binding_type(
+                re.as_ref(),
+                &envs,
+                state.table,
+                state.wildcard_vars,
+                strict,
+                state.resolver,
+            );
             type_check_(
                 state,
                 envs.clone(),
@@ -527,7 +569,14 @@ fn type_check_<L: Linearizer>(
             // Fields defined by interpolation are ignored.
             if let Term::RecRecord(..) = t.as_ref() {
                 for (id, rt) in stat_map {
-                    let tyw = binding_type(rt.as_ref(), &envs, state.table, strict, state.resolver);
+                    let tyw = binding_type(
+                        rt.as_ref(),
+                        &envs,
+                        state.table,
+                        state.wildcard_vars,
+                        strict,
+                        state.resolver,
+                    );
                     envs.insert(id.clone(), tyw.clone());
                     linearizer.retype_ident(lin, id, tyw);
                 }
@@ -723,21 +772,44 @@ fn type_check_<L: Linearizer>(
 ///       associated to `bound_exp`.
 /// As this function is always called in a context where an `ImportResolver` is present, expect
 /// it passed in arguments.
+///
+/// If the annotated type contains any wildcard:
+///     * in non strict mode, wildcards are assigned `Dyn`.
+///     * in strict mode, the wildcard is typechecked, and we return the unification variable
+///       corresponding to it.
 fn binding_type(
     t: &Term,
     envs: &Envs,
     table: &mut UnifTable,
+    wildcard_vars: &mut Vec<TypeWrapper>,
     strict: bool,
     resolver: &dyn ImportResolver,
 ) -> TypeWrapper {
     let ty_apt = apparent_type(t, Some(envs), Some(resolver));
 
     match ty_apt {
+        ApparentType::Annotated(ty) if strict => {
+            replace_wildcards_with_var(table, wildcard_vars, ty)
+        }
         ApparentType::Approximated(_) if strict => table.fresh_unif_var(),
         ty_apt => ty_apt.into(),
     }
 }
 
+/// Substitute wildcards in a type for their unification variable.
+fn replace_wildcards_with_var(
+    table: &mut UnifTable,
+    wildcard_vars: &mut Vec<TypeWrapper>,
+    ty: Types,
+) -> TypeWrapper {
+    match ty.0 {
+        AbsType::Wildcard(i) => get_wildcard_var(table, wildcard_vars, i),
+        _ => TypeWrapper::Concrete(
+            ty.0.map(|ty| Box::new(replace_wildcards_with_var(table, wildcard_vars, *ty))),
+        ),
+    }
+}
+
 /// Different kinds of apparent types (see [`apparent_type`]).
 ///
 /// Indicate the nature of an apparent type. In particular, when in strict mode, the typechecker
@@ -745,6 +817,7 @@ fn binding_type(
 /// generating a fresh unification variable.  In non-strict mode, however, the approximation is the
 /// best we can do. This type allows the caller of `apparent_type` to determine which situation it
 /// is.
+#[derive(Debug)]
 pub enum ApparentType {
     /// The apparent type is given by a user-provided annotation, such as an `Assume`, a `Promise`,
     /// or a metavalue.
@@ -761,6 +834,7 @@ pub enum ApparentType {
 impl From<ApparentType> for Types {
     fn from(at: ApparentType) -> Self {
         match at {
+            ApparentType::Annotated(ty) if has_wildcards(&ty) => Types(AbsType::Dyn()),
             ApparentType::Annotated(ty)
             | ApparentType::Inferred(ty)
             | ApparentType::Approximated(ty) => ty,
@@ -772,6 +846,9 @@ impl From<ApparentType> for Types {
 impl From<ApparentType> for TypeWrapper {
     fn from(at: ApparentType) -> TypeWrapper {
         match at {
+            ApparentType::Annotated(ty) if has_wildcards(&ty) => {
+                TypeWrapper::Concrete(AbsType::Dyn())
+            }
             ApparentType::Annotated(ty)
             | ApparentType::Inferred(ty)
             | ApparentType::Approximated(ty) => ty.into(),
@@ -788,7 +865,7 @@ impl From<ApparentType> for TypeWrapper {
 ///
 /// The role of `apparent_type` is precisely to determine the type of `bound_exp`:
 /// - if `bound_exp` is annotated by an `Assume`, a `Promise` or a metavalue, return the
-///   user-provided type.
+///   user-provided type, unless that type is a wildcard.
 /// - if `bound_exp` is a constant (string, number, boolean or symbol) which type can be deduced
 ///   directly without unfolding the expression further, return the corresponding exact type.
 /// - if `bound_exp` is an array, return `Array Dyn`.
@@ -861,6 +938,24 @@ pub fn infer_type(t: &Term) -> TypeWrapper {
     }
 }
 
+/// Deeply check whether a type contains a wildcard.
+fn has_wildcards(ty: &Types) -> bool {
+    let mut has_wildcard = false;
+    ty.clone()
+        .traverse::<_, _, std::convert::Infallible>(
+            &mut |ty, has_wildcard| {
+                if ty.0.is_wildcard() {
+                    *has_wildcard = true;
+                }
+                Ok(ty)
+            },
+            &mut has_wildcard,
+            TraverseOrder::TopDown,
+        )
+        .unwrap();
+    has_wildcard
+}
+
 /// The types on which the unification algorithm operates, which may be either a concrete type, a
 /// type constant or a unification variable.
 #[derive(Clone, PartialEq, Debug)]
@@ -933,6 +1028,7 @@ impl TypeWrapper {
                 Concrete(AbsType::DynRecord(Box::new(def_ty.subst(id, to))))
             }
             Concrete(AbsType::Array(ty)) => Concrete(AbsType::Array(Box::new(ty.subst(id, to)))),
+            Concrete(AbsType::Wildcard(i)) => Concrete(AbsType::Wildcard(i)),
             Constant(x) => Constant(x),
             Ptr(x) => Ptr(x),
         }
@@ -1039,6 +1135,12 @@ pub fn unify_(
 
     // t1 and t2 are roots of the type
     match (t1, t2) {
+        // If either type is a wildcard, unify with the associated type var
+        (TypeWrapper::Concrete(AbsType::Wildcard(id)), ty2)
+        | (ty2, TypeWrapper::Concrete(AbsType::Wildcard(id))) => {
+            let ty1 = get_wildcard_var(state.table, state.wildcard_vars, id);
+            unify_(state, ty1, ty2)
+        }
         (TypeWrapper::Concrete(s1), TypeWrapper::Concrete(s2)) => match (s1, s2) {
             (AbsType::Dyn(), AbsType::Dyn()) => Ok(()),
             (AbsType::Num(), AbsType::Num()) => Ok(()),
@@ -1407,7 +1509,8 @@ fn constrain_var(state: &mut State, tyw: &TypeWrapper, p: usize) {
                 | AbsType::Sym()
                 | AbsType::Flat(_)
                 | AbsType::RowEmpty()
-                | AbsType::Var(_) => (),
+                | AbsType::Var(_)
+                | AbsType::Wildcard(_) => (),
                 AbsType::Array(tyw) => constrain_var_(state, HashSet::new(), tyw.as_ref(), p),
                 AbsType::RowExtend(id, tyw, rest) => {
                     constr.insert(id.clone());
@@ -1477,3 +1580,24 @@ pub fn constr_unify(
         Ok(())
     }
 }
+
+/// Get the typevar associated with a given wildcard ID.
+fn get_wildcard_var(
+    table: &mut UnifTable,
+    wildcard_vars: &mut Vec<TypeWrapper>,
+    id: usize,
+) -> TypeWrapper {
+    // If `id` is not in `wildcard_vars`, populate it with fresh vars up to `id`
+    if id >= wildcard_vars.len() {
+        wildcard_vars.extend((wildcard_vars.len()..=id).map(|_| table.fresh_unif_var()));
+    }
+    wildcard_vars[id].clone()
+}
+
+/// Convert a mapping from wildcard ID to type var, into a mapping from wildcard ID to concrete type.
+fn wildcard_vars_to_type(wildcard_vars: Vec<TypeWrapper>, table: &UnifTable) -> Wildcards {
+    wildcard_vars
+        .into_iter()
+        .map(|var| to_type(&table, var))
+        .collect()
+}
diff --git a/src/types.rs b/src/types.rs
index 3ccc4f1f..2bed8147 100644
--- a/src/types.rs
+++ b/src/types.rs
@@ -100,6 +100,8 @@ pub enum AbsType<Ty> {
     DynRecord(Ty /*, Ty  Row */),
     /// A parametrized array.
     Array(Ty),
+    /// A type wildcard, wrapping an ID unique within a given file.
+    Wildcard(usize),
 }
 
 impl<Ty> AbsType<Ty> {
@@ -130,6 +132,7 @@ impl<Ty> AbsType<Ty> {
             AbsType::StaticRecord(t) => Ok(AbsType::StaticRecord(f(t)?)),
             AbsType::DynRecord(t) => Ok(AbsType::DynRecord(f(t)?)),
             AbsType::Array(t) => Ok(AbsType::Array(f(t)?)),
+            AbsType::Wildcard(i) => Ok(AbsType::Wildcard(i)),
         }
     }
 
@@ -148,6 +151,10 @@ impl<Ty> AbsType<Ty> {
             AbsType::RowExtend(..) | AbsType::RowEmpty() | AbsType::Dyn()
         )
     }
+
+    pub fn is_wildcard(&self) -> bool {
+        matches!(self, AbsType::Wildcard(_))
+    }
 }
 
 #[derive(Clone, Debug)]
@@ -313,6 +320,7 @@ impl Types {
             AbsType::DynRecord(ref ty) => {
                 mk_app!(contract::dyn_record(), ty.subcontract(h, pol, sy)?)
             }
+            AbsType::Wildcard(_) => contract::dynamic(),
         };
 
         Ok(ctr)
@@ -392,7 +400,8 @@ impl Types {
             | AbsType::Sym()
             | AbsType::Var(_)
             | AbsType::RowEmpty()
-            | AbsType::Flat(_) => Ok(ty.0),
+            | AbsType::Flat(_)
+            | AbsType::Wildcard(_) => Ok(ty.0),
             AbsType::Forall(id, ty_inner) => (*ty_inner)
                 .traverse(f, state, order)
                 .map(|ty| AbsType::Forall(id, Box::new(ty))),
@@ -485,6 +494,7 @@ impl fmt::Display for Types {
                 AbsType::Arrow(_, _) => write!(f, "({}) -> {}", dom, codom),
                 _ => write!(f, "{} -> {}", dom, codom),
             },
+            AbsType::Wildcard(_) => write!(f, "_"),
         }
     }
 }
@@ -551,5 +561,10 @@ mod test {
         assert_format_eq("Num -> Array (Array Str) -> Num");
         assert_format_eq("Array (Num -> Num)");
         assert_format_eq("Array (Array (Array Dyn) -> Num)");
+
+        assert_format_eq("_");
+        assert_format_eq("_ -> _");
+        assert_format_eq("{x: _, y: Bool}");
+        assert_format_eq("{_: _}");
     }
 }


Test patch:
diff --git a/tests/pass/typechecking.ncl b/tests/pass/typechecking.ncl
index 9ffe18a8..3afe8a3c 100644
--- a/tests/pass/typechecking.ncl
+++ b/tests/pass/typechecking.ncl
@@ -192,6 +192,11 @@ let typecheck = [
   (string.split ".") : Str -> Array Str,
   (array.length [] == 0) : Bool,
   (array.map (fun x => x ++ "1") ["a", "b", "c"]) : Array Str,
+
+  # wildcards
+  ("hello" : _) : Str,
+  ((fun x => x + 1) : _ -> Num) : Num -> Num,
+  ({"foo" = 1} : {foo : _}) : {foo: Num}
 ] in
 
 true
diff --git a/tests/query.rs b/tests/query.rs
index ebdd4563..5596511c 100644
--- a/tests/query.rs
+++ b/tests/query.rs
@@ -1,5 +1,5 @@
 use nickel_lang::program::Program;
-use nickel_lang::term::{SharedTerm, Term};
+use nickel_lang::term::{MetaValue, SharedTerm, Term};
 
 #[test]
 pub fn test_query_metadata_basic() {
@@ -31,3 +31,57 @@ pub fn test_query_metadata_from_func() {
         panic!();
     }
 }
+
+#[test]
+pub fn test_query_with_wildcard() {
+    /// Checks whether `lhs` and `rhs` both evaluate to terms with the same static type
+    fn assert_types_eq(lhs: &str, rhs: &str) {
+        let term1 = Program::new_from_source(lhs.as_bytes(), "regr_tests")
+            .unwrap()
+            .query(None)
+            .unwrap();
+        let term2 = Program::new_from_source(rhs.as_bytes(), "regr_tests")
+            .unwrap()
+            .query(None)
+            .unwrap();
+        if let (
+            Term::MetaValue(MetaValue {
+                types: Some(contract1),
+                ..
+            }),
+            Term::MetaValue(MetaValue {
+                types: Some(contract2),
+                ..
+            }),
+        ) = (term1, term2)
+        {
+            assert_eq!(contract1.types, contract2.types);
+            assert_eq!(
+                contract1.label.types.as_ref(),
+                contract2.label.types.as_ref()
+            );
+        } else {
+            panic!();
+        }
+    }
+
+    // Without wildcard, the result has no type annotation
+    let mut program = Program::new_from_source("10".as_bytes(), "regr_tests").unwrap();
+    let result = program.query(None).unwrap();
+    assert!(!matches!(result, Term::MetaValue(_)));
+
+    // With a wildcard, there is a type annotation, inferred to be Num
+    assert_types_eq("10 : _", "10 : Num");
+
+    // Wildcard infers record type
+    assert_types_eq(
+        r#"{foo: Str = "quux"} : _"#,
+        r#"{foo: Str = "quux"} : {foo: Str}"#,
+    );
+
+    // Wildcard infers function type, infers inside `let`
+    assert_types_eq(
+        r#"let f : _ = fun x => x + 1 in f"#,
+        r#"(fun x => x + 1) : Num -> Num"#,
+    );
+}
diff --git a/tests/typecheck_fail.rs b/tests/typecheck_fail.rs
index 08c62f34..2117dec3 100644
--- a/tests/typecheck_fail.rs
+++ b/tests/typecheck_fail.rs
@@ -4,11 +4,12 @@ use nickel_lang::cache::resolvers::DummyResolver;
 use nickel_lang::error::TypecheckError;
 use nickel_lang::parser::{grammar, lexer};
 use nickel_lang::term::RichTerm;
-use nickel_lang::typecheck::{type_check_in_env, Environment};
-use nickel_lang::types::Types;
+use nickel_lang::typecheck::{type_check_in_env, Environment, TypeCheckingOutput};
+use nickel_lang::types::{AbsType, Types};
 
 fn type_check(rt: &RichTerm) -> Result<Types, TypecheckError> {
     type_check_in_env(rt, &Environment::new(), &mut DummyResolver {})
+        .map(|TypeCheckingOutput { types, .. }| types)
 }
 
 fn type_check_expr(s: impl std::string::ToString) -> Result<Types, TypecheckError> {
@@ -230,6 +231,7 @@ fn piecewise_signature() {
         Err(TypecheckError::TypeMismatch(..))
     );
 }
+
 #[test]
 fn recursive_let() {
     assert_matches!(
@@ -237,3 +239,42 @@ fn recursive_let() {
         Err(TypecheckError::TypeMismatch(..))
     );
 }
+
+#[test]
+fn fails_only_with_wildcard() {
+    // Without a wildcard annotation, this type checks
+    assert_matches!(
+        type_check_expr("let head = fun l => %head% l in head 10"),
+        Ok(_)
+    );
+    // However, with one, we get a type error
+    assert_matches!(
+        type_check_expr("(let head = fun l => %head% l in (head 10)) : _"),
+        Err(TypecheckError::TypeMismatch(..))
+    );
+    // With an actual array, this passes
+    assert_matches!(
+        type_check_expr("(let head = fun l => %head% l in (head [10])) : _"),
+        Ok(_)
+    );
+}
+
+#[test]
+fn wildcards_apparent_type_is_dyn() {
+    // Wildcard-inferred types don't leak outside of the strict block.
+    // Therefore, even though the body of `g` could type check, `f` has type
+    // `Dyn`, exactly as if there were no wildcards, and the type checker
+    // rejects the expression.
+    assert_matches!(
+        type_check_expr(
+            r#"let f : _ -> _ = fun x => x + 1 in
+let g : Num = f 0 in
+g"#
+        ),
+        Err(TypecheckError::TypeMismatch(
+            Types(AbsType::Arrow(_, _)),
+            Types(AbsType::Dyn()),
+            _
+        ))
+    );
+}