Context Navigation

Changes between Version 38 and Version 39 of Records/NameSpacing

v38	v39
70	70	Here's a complex example:
71	71
	72	{{{
72	73	type family F a b
73	74	data instance F Int [a] = Mk { f :: Int }
…	…
77	78
78	79	k x = (g x, x.f, h x)
	80	}}}
79	81
80	82	Consider type inference on k. Initially we know nothing about the
…	…
106	108	and solving them later. We express it like this:
107	109
	110	{{{
108	111	G, r:t1 \|- r.f : t2, (Has t1 "f" t2)
	112	}}}
109	113
110	114	This says that if r is in scope with type t1, then (r.f) has type t2,
111	115	plus the constraint (Has t1 "f" t2), which we read as saying
112	116
	117	{{{
113	118	Type t1 must have a field "f" of type t2
	119	}}}
114	120
115	121	We gather up all the constraints and solve them. In solving them