Skip to content

Commit 9ee7974

Browse files
purefunctorpurefunctor
committed
Begin implementing kind checker for data declaration
1 parent 164357b commit 9ee7974

File tree

7 files changed

+195
-15
lines changed

7 files changed

+195
-15
lines changed

‎compiler-core/checking/src/check/convert.rs‎

Lines changed: 43 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -90,9 +90,51 @@ where
9090
}
9191
}
9292

93+
/// A variant of [`type_to_core`] for use with signature declarations.
94+
///
95+
/// Unlike the regular [`type_to_core`], this function does not call
96+
/// [`CheckState::unbind`] after each [`lowering::TypeKind::Forall`]
97+
/// node. This allows type variables to be scoped for the entire
98+
/// declaration group rather than just the type signature.
99+
pub fn signature_type_to_core<Q>(
100+
state: &mut CheckState,
101+
context: &CheckContext<Q>,
102+
id: lowering::TypeId,
103+
) -> TypeId
104+
where
105+
Q: ExternalQueries,
106+
{
107+
let default = context.prim.unknown;
108+
109+
let Some(kind) = context.lowered.info.get_type_kind(id) else {
110+
return default;
111+
};
112+
113+
match kind {
114+
lowering::TypeKind::Forall { bindings, type_ } => {
115+
let binders = bindings
116+
.iter()
117+
.map(|binding| convert_forall_binding(state, context, binding))
118+
.collect_vec();
119+
120+
let inner = type_.map_or(default, |id| type_to_core(state, context, id));
121+
122+
binders
123+
.into_iter()
124+
.rfold(inner, |inner, binder| state.storage.intern(Type::Forall(binder, inner)))
125+
}
126+
127+
lowering::TypeKind::Parenthesized { parenthesized } => {
128+
parenthesized.map(|id| signature_type_to_core(state, context, id)).unwrap_or(default)
129+
}
130+
131+
_ => type_to_core(state, context, id),
132+
}
133+
}
134+
93135
const INVALID_NAME: SmolStr = SmolStr::new_inline("<invalid>");
94136

95-
fn convert_forall_binding<Q>(
137+
pub fn convert_forall_binding<Q>(
96138
state: &mut CheckState,
97139
context: &CheckContext<Q>,
98140
binding: &lowering::TypeVariableBinding,

‎compiler-core/checking/src/check/unification.rs‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,26 @@ use crate::ExternalQueries;
77
use crate::check::{CheckContext, CheckState, kind};
88
use crate::core::{Type, TypeId, Variable, debruijn};
99

10+
pub fn subsumes<Q>(
11+
state: &mut CheckState,
12+
context: &CheckContext<Q>,
13+
t1: TypeId,
14+
t2: TypeId,
15+
) -> bool
16+
where
17+
Q: ExternalQueries,
18+
{
19+
let t1 = state.normalize_type(t1);
20+
let t2 = state.normalize_type(t2);
21+
match (&state.storage[t1], &state.storage[t2]) {
22+
(&Type::Function(t1_argument, t1_result), &Type::Function(t2_argument, t2_result)) => {
23+
subsumes(state, context, t2_argument, t1_argument)
24+
&& subsumes(state, context, t1_result, t2_result)
25+
}
26+
_ => unify(state, context, t1, t2),
27+
}
28+
}
29+
1030
pub fn unify<Q>(state: &mut CheckState, context: &CheckContext<Q>, t1: TypeId, t2: TypeId) -> bool
1131
where
1232
Q: ExternalQueries,

‎compiler-core/checking/src/core/pretty.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -89,7 +89,7 @@ fn traverse<'a, Q: ExternalQueries>(source: &mut TraversalSource<'a, Q>, id: Typ
8989
}
9090

9191
let inner = traverse(source, inner);
92-
write!(&mut buffer, " {inner}").unwrap();
92+
write!(&mut buffer, ". {inner}").unwrap();
9393

9494
buffer
9595
}

‎compiler-core/checking/src/lib.rs‎

Lines changed: 80 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,14 @@ use std::sync::Arc;
88
use building_types::{QueryProxy, QueryResult};
99
use files::FileId;
1010
use indexing::{IndexedModule, TermItemId, TypeItemId};
11-
use lowering::{LoweredModule, Scc};
11+
use itertools::Itertools;
12+
use lowering::{DataIr, LoweredModule, Scc, TermItemIr, TypeItemIr, TypeVariableBinding};
1213
use resolving::ResolvedModule;
1314
use rustc_hash::FxHashMap;
1415

15-
use crate::check::{CheckContext, CheckState, kind, transfer};
16-
use crate::core::{ForallBinder, Variable, debruijn};
16+
use crate::check::kind::check_surface_kind;
17+
use crate::check::{CheckContext, CheckState, convert, kind, transfer};
18+
use crate::core::{ForallBinder, Variable, debruijn, pretty};
1719

1820
pub trait ExternalQueries:
1921
QueryProxy<
@@ -85,26 +87,95 @@ where
8587
{
8688
let Some(item) = context.lowered.info.get_type_item(item_id) else { return };
8789
match item {
88-
lowering::TypeItemIr::DataGroup { .. } => (),
90+
TypeItemIr::DataGroup { signature, data, .. } => {
91+
let signature_type = signature
92+
.map(|signature| convert::signature_type_to_core(state, context, signature));
93+
94+
if let Some(DataIr { variables }) = data {
95+
let inferred_type = create_type_declaration_kind(state, context, &variables);
96+
for constructor_id in context.indexed.pairs.data_constructors(item_id) {
97+
let Some(TermItemIr::Constructor { arguments }) =
98+
context.lowered.info.get_term_item(constructor_id)
99+
else {
100+
continue;
101+
};
102+
for argument in arguments.iter() {
103+
let (inferred_type, inferred_kind) =
104+
check_surface_kind(state, context, *argument, context.prim.t);
105+
{
106+
let inferred_type = pretty::print_local(state, context, inferred_type);
107+
let inferred_kind = pretty::print_local(state, context, inferred_kind);
108+
eprintln!("{inferred_type} :: {inferred_kind}")
109+
}
110+
}
111+
}
112+
113+
{
114+
if let Some(signature_type) = signature_type {
115+
let signature_type = pretty::print_local(state, context, signature_type);
116+
eprintln!("{signature_type}");
117+
}
118+
let inferred_type = pretty::print_local(state, context, inferred_type);
119+
eprintln!("{inferred_type}");
120+
}
121+
}
122+
}
89123

90-
lowering::TypeItemIr::NewtypeGroup { .. } => (),
124+
TypeItemIr::NewtypeGroup { .. } => (),
91125

92-
lowering::TypeItemIr::SynonymGroup { .. } => (),
126+
TypeItemIr::SynonymGroup { .. } => (),
93127

94-
lowering::TypeItemIr::ClassGroup { .. } => (),
128+
TypeItemIr::ClassGroup { .. } => (),
95129

96-
lowering::TypeItemIr::Foreign { signature, .. } => {
130+
TypeItemIr::Foreign { signature, .. } => {
97131
let Some(signature_id) = signature else { return };
98132
let (inferred_type, _) =
99133
kind::check_surface_kind(state, context, *signature_id, context.prim.t);
100134
let inferred_type = transfer::globalize(state, context, inferred_type);
101135
state.checked.types.insert(item_id, inferred_type);
102136
}
103137

104-
lowering::TypeItemIr::Operator { .. } => (),
138+
TypeItemIr::Operator { .. } => (),
105139
}
106140
}
107141

142+
fn create_type_declaration_kind<Q>(
143+
state: &mut CheckState,
144+
context: &CheckContext<Q>,
145+
bindings: &[TypeVariableBinding],
146+
) -> TypeId
147+
where
148+
Q: ExternalQueries,
149+
{
150+
let binders = bindings
151+
.iter()
152+
.map(|binding| convert::convert_forall_binding(state, context, binding))
153+
.collect_vec();
154+
155+
// Build the function type for the type declaration e.g.
156+
//
157+
// ```purescript
158+
// data Maybe a = Just a | Nothing
159+
// ```
160+
//
161+
// function_type := a -> Type
162+
let size = state.bound.size();
163+
let function_type = binders.iter().rfold(context.prim.t, |result, binder| {
164+
let index = binder.level.to_index(size).unwrap_or_else(|| {
165+
unreachable!("invariant violated: invalid {} for {size}", binder.level)
166+
});
167+
let variable = state.storage.intern(Type::Variable(Variable::Bound(index)));
168+
state.storage.intern(Type::Function(variable, result))
169+
});
170+
171+
// Qualify the type variables in the function type e.g.
172+
//
173+
// forall (a :: Type). a -> Type
174+
binders
175+
.into_iter()
176+
.rfold(function_type, |inner, binder| state.storage.intern(Type::Forall(binder, inner)))
177+
}
178+
108179
fn prim_check_module(
109180
queries: &impl ExternalQueries,
110181
file_id: FileId,

‎tests-integration/tests/checking.rs‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -275,13 +275,13 @@ fn test_quantify_multiple_scoped() {
275275
fn test_manual() {
276276
let (engine, id) = empty_engine();
277277

278-
engine.set_content(id, "module Main where\n\nforeign import data T :: Proxy 123");
278+
engine.set_content(id, "module Main where\n\ndata Either a b = Left a | Right b");
279279

280280
let resolved = engine.resolved(id).unwrap();
281281
let checked = engine.checked(id).unwrap();
282282

283-
let (_, id) = resolved.locals.lookup_type("T").unwrap();
284-
let id = checked.lookup_type(id).unwrap();
283+
// let (_, id) = resolved.locals.lookup_type("T").unwrap();
284+
// let id = checked.lookup_type(id).unwrap();
285285

286-
eprintln!("{}", pretty::print_global(&engine, id));
286+
// eprintln!("{}", pretty::print_global(&engine, id));
287287
}

‎tests-integration/tests/lowering_scc.rs‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,3 +77,32 @@ infix 5 type Add as +
7777

7878
insta::assert_debug_snapshot!((terms, types));
7979
}
80+
81+
#[test]
82+
fn test_non_cycle_ordering() {{
83+
let mut engine = QueryEngine::default();
84+
let mut files = Files::default();
85+
prim::configure(&mut engine, &mut files);
86+
87+
let id = files.insert(
88+
"Main.purs",
89+
r#"
90+
module Main where
91+
92+
a _ = b 0
93+
b _ = c 0
94+
c _ = 0
95+
"#,
96+
);
97+
let content = files.content(id);
98+
99+
engine.set_content(id, content);
100+
101+
let lowered = engine.lowered(id).unwrap();
102+
103+
let terms = &lowered.term_scc;
104+
let types = &lowered.type_scc;
105+
106+
insta::assert_debug_snapshot!((terms, types));
107+
}
108+
}

‎tests-integration/tests/snapshots/lowering_scc__non_cycle_ordering.snap‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
---
2+
source: tests-integration/tests/lowering_scc.rs
3+
expression: "(terms, types)"
4+
---
5+
(
6+
[
7+
Base(
8+
Idx::<TermItem>(2),
9+
),
10+
Base(
11+
Idx::<TermItem>(1),
12+
),
13+
Base(
14+
Idx::<TermItem>(0),
15+
),
16+
],
17+
[],
18+
)

0 commit comments

Comments
 (0)