Safe Haskell | None |
---|---|

Language | Haskell2010 |

## Synopsis

- shad :: uni `Includes` Integer => Type TyName uni ()
- mkShad :: uni `Includes` Integer => Term TyName Name uni fun ()
- recUnit :: uni `Includes` () => Type TyName uni ()
- runRecUnit :: uni `Includes` () => Term TyName Name uni fun ()

# Documentation

mkShad :: uni `Includes` Integer => Term TyName Name uni fun () Source #

Test that shadowing does not result in variable capture. The definition is as follows:

/\(a :: *) -> wrap (getShadF a) a (\(x : a) -> /\(f :: * -> *) -> \(y : f i) -> 0)

Type checking this term we eventually reach

NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case `vPat`

is `shadF`

and `arg`

is `a`

), which, if we were naive,
would unfold into

a -> all (a :: * -> *). a a -> integer

i.e. we substituted the outer `a`

for `i`

, but due to variable capture via `all`

that outer `a`

now became an inner one, which would be a bug.

But that problem is already solved before type checking starts as we rename the program and that makes all binders uniques, so no variable capture is possible due to the outer and inner bindings being distinct.

runRecUnit :: uni `Includes` () => Term TyName Name uni fun () Source #

Test that a binder in a pattern functor does not get duplicated. The definition is as follows:

/\(a :: *) -> \(ru : recUnit) -> unwrap ru {a} ru

Type checking this term we eventually reach

NORM (vPat (\(a :: k) -> ifix vPat a) arg)

(where in our case `vPat`

is `recUnitF`

and `arg`

is `()`

), which, if we were naive,
would unfold into

all (r :: *). ifix (\(rec :: * -> *) (i :: *) -> all (r :: *). rec i -> r -> r) () -> r -> r

and break global uniqueness as the `all (r :: *)`

binder appears twice.

But this doesn't happen in the actual code, since when a variable gets looked up during type normalization, its value gets renamed, which means that a fresh variable will be generated for the inner binder and there will be no shadowing.