Scoping rules

Implicit Arguments

Given the following:

infixr 5 ~>
(~>) : {ix : Type} -> (ix -> Type) -> (ix -> Type) -> Type
(~>) {ix} f g = (i : ix) -> f i -> g i

imap : (a ~> b) -> (Id a) ~> (Id b)
imap f i (MkIId x) = MkIId (f i x)

The arguments a and b to imap are implicit and are available for use in the body of imap by pattern matching them with {}. For this reason, it might be confusing if we had MkIId a as one would normally expect a to be referring to the implicit argument and not a parameter to MkIId

“Prefer letting all the arguments have distinct names - even if one is only named in the type declaration and the other only in the body.”

When confused about what’s implicit, we can ask the REPL. :t will show implicit arguments by underlining them. We can also use :set showimplicits to really see what’s going on behind the scenes.


Metavariables (which to me are holes) have global scope, which can be confusing:

iskip : a ~> Id a
iskip i a = ?a

iextend : (a ~> Id b) -> Id a ~> Id b
iextend f i (MkIId x) = f i x

This code won’t type check, because ?a introduces a metavariable that will be used in iextend. Instead, it would be better to rename ?a to ?iskip_rhs.

The reason metavariables have global scope is because we can prove them later, which appends their proof to the end of the file. We’re also able to ask their type, so they need to be available at the top level.



Colours have special meanings in the REPL:

The colour of bound variables