Extern types

chalk-integration/src/lowering.rs

@@ -2,8 +2,9 @@ use crate::interner::{ChalkFnAbi, ChalkIr};
 use chalk_ir::cast::{Cast, Caster};
 use chalk_ir::interner::{HasInterner, Interner};
 use chalk_ir::{
-    self, AdtId, AssocTypeId, BoundVar, ClausePriority, ClosureId, DebruijnIndex, FnDefId, ImplId,
-    OpaqueTyId, QuantifiedWhereClauses, Substitution, ToGenericArg, TraitId, TyKind, VariableKinds,
+    self, AdtId, AssocTypeId, BoundVar, ClausePriority, ClosureId, DebruijnIndex, ExternDefId,
+    FnDefId, ImplId, OpaqueTyId, QuantifiedWhereClauses, Substitution, ToGenericArg, TraitId,
+    TyKind, VariableKinds,
 };
 use chalk_parse::ast::*;
 use chalk_solve::rust_ir::{
@@ -33,6 +34,7 @@ type OpaqueTyKinds = BTreeMap<chalk_ir::OpaqueTyId<ChalkIr>, TypeKind>;
 type AssociatedTyLookups = BTreeMap<(chalk_ir::TraitId<ChalkIr>, Ident), AssociatedTyLookup>;
 type AssociatedTyValueIds =
     BTreeMap<(chalk_ir::ImplId<ChalkIr>, Ident), AssociatedTyValueId<ChalkIr>>;
+type ExternIds = BTreeMap<Ident, chalk_ir::ExternDefId<ChalkIr>>;
 
 type ParameterMap = BTreeMap<Ident, chalk_ir::WithKind<ChalkIr, BoundVar>>;
 
@@ -53,6 +55,7 @@ struct Env<'k> {
     opaque_ty_kinds: &'k OpaqueTyKinds,
     associated_ty_lookups: &'k AssociatedTyLookups,
     auto_traits: &'k AutoTraits,
+    extern_ty_ids: &'k ExternIds,
     /// GenericArg identifiers are used as keys, therefore
     /// all identifiers in an environment must be unique (no shadowing).
     parameter_map: ParameterMap,
@@ -177,6 +180,16 @@ impl<'k> Env<'k> {
                 .cast(interner),
             );
         }
+
+        if let Some(id) = self.extern_ty_ids.get(&name.str) {
+            return Ok(chalk_ir::TyData::Apply(chalk_ir::ApplicationTy {
+                name: chalk_ir::TypeName::Extern(*id),
+                substitution: chalk_ir::Substitution::empty(interner),
+            })
+            .intern(interner)
+            .cast(interner));
+        }
+
         if let Some(_) = self.trait_ids.get(&name.str) {
             return Err(RustIrError::NotStruct(name.clone()));
         }
@@ -408,6 +421,7 @@ impl LowerProgram for Program {
                 }
                 Item::Impl(_) => continue,
                 Item::Clause(_) => continue,
+                Item::Extern(_) => continue,
             };
         }
 
@@ -425,6 +439,8 @@ impl LowerProgram for Program {
         let mut opaque_ty_data = BTreeMap::new();
         let mut hidden_opaque_types = BTreeMap::new();
         let mut custom_clauses = Vec::new();
+        let mut extern_ty_ids = BTreeMap::new();
+
         for (item, &raw_id) in self.items.iter().zip(&raw_ids) {
             let empty_env = Env {
                 adt_ids: &adt_ids,
@@ -441,6 +457,7 @@ impl LowerProgram for Program {
                 associated_ty_lookups: &associated_ty_lookups,
                 parameter_map: BTreeMap::new(),
                 auto_traits: &auto_traits,
+                extern_ty_ids: &extern_ty_ids,
             };
 
             match *item {
@@ -638,6 +655,9 @@ impl LowerProgram for Program {
                         );
                     }
                 }
+                Item::Extern(ExternDefn(ref ident)) => {
+                    extern_ty_ids.insert(ident.str.clone(), ExternDefId(raw_id));
+                }
             }
         }
 
@@ -667,6 +687,7 @@ impl LowerProgram for Program {
             hidden_opaque_types,
             custom_clauses,
             object_safe_traits,
+            extern_ty_ids,
         };
 
         Ok(program)
@@ -2016,6 +2037,7 @@ impl LowerGoal<LoweredProgram> for Goal {
             trait_kinds: &program.trait_kinds,
             opaque_ty_kinds: &program.opaque_ty_kinds,
             associated_ty_lookups: &associated_ty_lookups,
+            extern_ty_ids: &program.extern_ty_ids,
             parameter_map: BTreeMap::new(),
             auto_traits: &auto_traits,
         };

chalk-integration/src/program.rs

@@ -4,8 +4,8 @@ use chalk_ir::could_match::CouldMatch;
 use chalk_ir::debug::Angle;
 use chalk_ir::{
     debug::SeparatorTraitRef, AdtId, AliasTy, ApplicationTy, AssocTypeId, Binders,
-    CanonicalVarKinds, ClosureId, FnDefId, GenericArg, Goal, Goals, ImplId, Lifetime, OpaqueTy,
-    OpaqueTyId, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy,
+    CanonicalVarKinds, ClosureId, ExternDefId, FnDefId, GenericArg, Goal, Goals, ImplId, Lifetime,
+    OpaqueTy, OpaqueTyId, ProgramClause, ProgramClauseImplication, ProgramClauses, ProjectionTy,
     Substitution, TraitId, Ty,
 };
 use chalk_solve::rust_ir::{
@@ -89,6 +89,9 @@ pub struct Program {
 
     /// Store the traits marked with `#[object_safe]`
     pub object_safe_traits: HashSet<TraitId<ChalkIr>>,
+
+    /// For each extern type `extern { type A; }`
+    pub extern_ty_ids: BTreeMap<Identifier, ExternDefId<ChalkIr>>,
 }
 
 impl Program {

chalk-ir/src/debug.rs

@@ -35,6 +35,13 @@ impl<I: Interner> Debug for ClosureId<I> {
     }
 }
 
+impl<I: Interner> Debug for ExternDefId<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> std::fmt::Result {
+        I::debug_extern_def_id(*self, fmt)
+            .unwrap_or_else(|| write!(fmt, "ExternDefId({:?})", self.0))
+    }
+}
+
 impl<I: Interner> Debug for Ty<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         I::debug_ty(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
@@ -184,6 +191,7 @@ impl<I: Interner> Debug for TypeName<I> {
             TypeName::Never => write!(fmt, "Never"),
             TypeName::Array => write!(fmt, "{{array}}"),
             TypeName::Closure(id) => write!(fmt, "{{closure:{:?}}}", id),
+            TypeName::Extern(extern_ty) => write!(fmt, "{:?}", extern_ty),
             TypeName::Error => write!(fmt, "{{error}}"),
         }
     }

chalk-ir/src/fold/boring_impls.rs

@@ -303,6 +303,7 @@ id_fold!(AssocTypeId);
 id_fold!(OpaqueTyId);
 id_fold!(FnDefId);
 id_fold!(ClosureId);
+id_fold!(ExternDefId);
 
 impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClauseData<I> {
     fn super_fold_with<'i>(

chalk-ir/src/interner.rs

@@ -8,6 +8,7 @@ use crate::CanonicalVarKinds;
 use crate::ClosureId;
 use crate::Constraint;
 use crate::Constraints;
+use crate::ExternDefId;
 use crate::FnDefId;
 use crate::GenericArg;
 use crate::GenericArgData;
@@ -245,6 +246,16 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
         None
     }
 
+    /// Prints the debug representation of a extern-def-id.
+    /// Returns `None` to fallback to the default debug output.
+    #[allow(unused_variables)]
+    fn debug_extern_def_id(
+        extern_def_id: ExternDefId<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result> {
+        None
+    }
+
     /// Prints the debug representation of an alias.
     /// Returns `None` to fallback to the default debug output.
     #[allow(unused_variables)]

chalk-ir/src/lib.rs

@@ -254,6 +254,9 @@ pub enum TypeName<I: Interner> {
     /// A closure.
     Closure(ClosureId<I>),
 
+    /// extern types
+    Extern(ExternDefId<I>),
+
     /// This can be used to represent an error, e.g. during name resolution of a type.
     /// Chalk itself will not produce this, just pass it through when given.
     Error,
@@ -363,6 +366,10 @@ pub struct FnDefId<I: Interner>(pub I::DefId);
 #[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
 pub struct ClosureId<I: Interner>(pub I::DefId);
 
+/// Id for extern types.
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
+pub struct ExternDefId<I: Interner>(pub I::DefId);
+
 impl_debugs!(ImplId, ClauseId);
 
 /// A Rust type. The actual type data is stored in `TyData`.

chalk-ir/src/visit/boring_impls.rs

@@ -5,10 +5,11 @@
 //! The more interesting impls of `Visit` remain in the `visit` module.
 
 use crate::{
-    AdtId, AssocTypeId, ClausePriority, ClosureId, Constraints, DebruijnIndex, FloatTy, FnDefId,
-    GenericArg, Goals, ImplId, IntTy, Interner, Mutability, OpaqueTyId, PlaceholderIndex,
-    ProgramClause, ProgramClauses, QuantifiedWhereClauses, QuantifierKind, Safety, Scalar,
-    Substitution, SuperVisit, TraitId, UintTy, UniverseIndex, Visit, VisitResult, Visitor,
+    AdtId, AssocTypeId, ClausePriority, ClosureId, Constraints, DebruijnIndex, ExternDefId,
+    FloatTy, FnDefId, GenericArg, Goals, ImplId, IntTy, Interner, Mutability, OpaqueTyId,
+    PlaceholderIndex, ProgramClause, ProgramClauses, QuantifiedWhereClauses, QuantifierKind,
+    Safety, Scalar, Substitution, SuperVisit, TraitId, UintTy, UniverseIndex, Visit, VisitResult,
+    Visitor,
 };
 use std::{marker::PhantomData, sync::Arc};
 
@@ -239,6 +240,7 @@ id_visit!(OpaqueTyId);
 id_visit!(AssocTypeId);
 id_visit!(FnDefId);
 id_visit!(ClosureId);
+id_visit!(ExternDefId);
 
 impl<I: Interner> SuperVisit<I> for ProgramClause<I> {
     fn super_visit_with<'i, R: VisitResult>(

chalk-parse/src/ast.rs

@@ -27,8 +27,12 @@ pub enum Item {
     OpaqueTyDefn(OpaqueTyDefn),
     Impl(Impl),
     Clause(Clause),
+    Extern(ExternDefn),
 }
 
+#[derive(Clone, PartialEq, Eq, Debug)]
+pub struct ExternDefn(pub Identifier);
+
 #[derive(Clone, PartialEq, Eq, Debug)]
 pub struct AdtDefn {
     pub name: Identifier,

chalk-parse/src/parser.lalrpop

@@ -20,6 +20,11 @@ Item: Option<Item> = {
     OpaqueTyDefn => Some(Item::OpaqueTyDefn(<>)),
     Impl => Some(Item::Impl(<>)),
     Clause => Some(Item::Clause(<>)),
+    ExternType => Some(Item::Extern(<>)),
+};
+
+ExternType: ExternDefn = {
+    "extern" "{" "type" <id:Id> ";" "}" => ExternDefn(id),
 };
 
 Comment: () = r"//.*";

chalk-solve/src/clauses.rs

@@ -635,7 +635,8 @@ fn match_type_name<I: Interner>(
         | TypeName::Ref(_)
         | TypeName::Array
         | TypeName::Never
-        | TypeName::Closure(_) => {
+        | TypeName::Closure(_)
+        | TypeName::Extern(_) => {
             builder.push_fact(WellFormed::Ty(application.clone().intern(interner)))
         }
     }

chalk-solve/src/clauses/builtin_traits/copy.rs

@@ -75,6 +75,7 @@ pub fn add_copy_program_clauses<I: Interner>(
             | TypeName::AssociatedType(_)
             | TypeName::Slice
             | TypeName::OpaqueType(_)
+            | TypeName::Extern(_)
             | TypeName::Error => {}
         },
 

chalk-solve/src/clauses/builtin_traits/sized.rs

@@ -93,6 +93,7 @@ pub fn add_sized_program_clauses<I: Interner>(
             | TypeName::Slice
             | TypeName::OpaqueType(_)
             | TypeName::Str
+            | TypeName::Extern(_)
             | TypeName::Error => {}
         },
 

chalk-solve/src/display/ty.rs

@@ -217,6 +217,7 @@ impl<I: Interner> RenderAsRust<I> for ApplicationTy<I> {
             // FIXME: write out valid types for these variants
             TypeName::FnDef(_) => write!(f, "<fn_def>")?,
             TypeName::Closure(..) => write!(f, "<closure>")?,
+            TypeName::Extern(_) => write!(f, "<extern>")?,
 
             TypeName::Array => write!(
                 f,

tests/test/extern_types.rs

@@ -0,0 +1,72 @@
+//! Tests for extern types
+
+use super::*;
+
+#[test]
+fn extern_ty_trait_impl() {
+    test! {
+        program {
+            extern { type A; }
+            trait Foo {}
+            impl Foo for A {}
+        }
+
+        goal { A: Foo } yields { "Unique" }
+    }
+}
+
+#[test]
+fn extern_ty_single() {
+    lowering_success! {
+        program {
+            extern { type A; }
+        }
+    }
+}
+
+#[test]
+fn extern_ty_is_well_formed() {
+    test! {
+        program {
+            extern { type A; }
+        }
+
+        goal { WellFormed(A) } yields { "Unique" }
+    }
+}
+
+#[test]
+fn extern_ty_is_not_sized() {
+    test! {
+        program {
+            #[lang(sized)] trait Sized {}
+            extern { type A; }
+        }
+
+        goal { not { A: Sized } } yields { "Unique" }
+    }
+}
+
+#[test]
+fn extern_ty_is_not_copy() {
+    test! {
+        program {
+            #[lang(copy)] trait Copy {}
+            extern { type A; }
+        }
+
+        goal { not { A: Copy } } yields { "Unique" }
+    }
+}
+
+#[test]
+fn extern_ty_is_not_clone() {
+    test! {
+        program {
+            #[lang(clone)] trait Clone {}
+            extern { type A; }
+        }
+
+        goal { not { A: Clone } } yields { "Unique" }
+    }
+}

tests/test/mod.rs

@@ -328,6 +328,7 @@ mod coinduction;
 mod constants;
 mod cycle;
 mod existential_types;
+mod extern_types;
 mod fn_def;
 mod implied_bounds;
 mod impls;