I'm trying to implement a toy regular type system that ensures a few well formediness side constraints and allows for unfolding mu bindings in it. The data type representing these types contains constructors for fixed point (Mu), replacement by the nearest enclosing Mu-bound term (Var), and zero and one argument type operators (Nullary and Unary, respectively).
To ensure some that these types are well-formed they track, as three Bool parameters, whether they have a Mu as their head constructor, a Var as their head constructor, or a Var anywhere within them.
data A : Bool -- Is Mu headed?
-> Bool -- Is Var headed?
-> Bool -- Contains any Var's?
-> Type where
Mu : A False False _ -> A True False False
Var : A False True True
Nullary : A False False False
Unary : A _ _ m -> A False False m
To implement unfolding for Mu-headed types I need to perform substitutions, specifically I need to implement "Mu x. F ====> F[(Mu x. F)/x]".
Other than needing some to generate a proof that the third type parameter works out, the function subst seems straightforward:
total subst : A m1 v1 c1 -> A m2 v2 c2 -> (c3 ** ((A (m2 || (v2 && m1))
(v2 && v1)
c3)
,(c3 = (c2 && c1))))
subst _ Nullary = (_ ** (Nullary,Refl))
subst w (Unary a) with (subst w a)
| (c3** (a',aeq)) = (c3 ** (Unary a',aeq))
subst w Var = (_ ** (w,Refl))
subst w (Mu a) = (_ ** (Mu a,Refl))
I tried and failed to write a wrapper that cleans up this return type a bit.
total subst' : A m1 v1 c1 -> A m2 v2 c2 -> A (m2 || (v2 && m1))
(v2 && v1)
(c2 && c1)
subst' a1 a2 with (subst a2 a2)
| (_**(a',aeq)) ?= a'
When I try to solve this metavariable, I find that aeq : x = c2 && Delay c2 not aeq : x = c2 && Delay c1 as I expected (recall that (&&) is lazy in its second argument).
Am I doing something wrong? Is this the expected behaviour? FWIW, I successfully wrote a very similar wrapper for unfold (not shown).
Bool. – dfeuer