Commit b5647315 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Comments (TcSMonad)

parent 52b02e66
......@@ -705,6 +705,9 @@ A generalised substitution S is "inert" iff
(IG2) if (b -f-> t) in S, and f >= f, then S(f,t) = t
that is, each individual binding is "self-stable"
By (IG1) we define S*(f,t) to be the result of exahaustively
applying S(f,_) to t.
----------------------------------------------------------------
Our main invariant:
the inert CTyEqCans should be an inert generalised substitution
......@@ -737,7 +740,8 @@ This is the main theorem!
or (K2c) not (fw >= fs)
or (K2d) a not in s
(K3) If (b -fs-> s) is in S with (fw >= fs), then
(K3) See Note [K3: completeness of solving]
If (b -fs-> s) is in S with (fw >= fs), then
(K3a) If the role of fs is nominal: s /= a
(K3b) If the role of fs is representational: EITHER
a not in s, OR
......@@ -818,9 +822,9 @@ Key lemma to make it watertight.
Also, consider roles more carefully. See Note [Flavours with roles].
Completeness
~~~~~~~~~~~~~
K3: completeness. (K3) is not necessary for the extended substitution
Note [K3: completeness of solving]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
(K3) is not necessary for the extended substitution
to be inert. In fact K1 could be made stronger by saying
... then (not (fw >= fs) or not (fs >= fs))
But it's not enough for S to be inert; we also want completeness.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment