Applying close over Shift at level 0 should not be an error.

[lambdageek]

(Found this while working on adding Shift to unbound-generics (see lambdageek/unbound-generics@0d2467e16d993224de9e3cfa0379dbdb26896699).

When close is applied to a Shift at level 0, the library throws an error. But consider the following example (which I believe to be sensible):

type Var = Name Term

data Term
  = V Var
  | Pi (Bind (Var, Embed Term) Term)
  | LetRec (Bind (Rec Decl) Term)
    deriving (Show)

data Decl =
  -- a recursive declaration  x : A = m
  -- where x may occur in m but not in A
  Decl {
    declVar :: Var
    , declClass :: Shift (Embed Term)
    , declVal :: Embed Term
    }
  deriving (Show)

$(derive [''Term, ''Decl])

instance Alpha Term
instance Alpha Decl

Here the intent is that the classifier of a recursive binding should not refer to the binding itself, but to an outer scope.

x :: Var
x = s2n "x"

letrec :: Decl -> Term -> Term
letrec d e = LetRec $ bind (rec d) e

decl :: Var -> Term -> Term -> Decl
decl v klass e = Decl v (embed klass) (embed e)

-- >> show m1
-- "LetRec (<[Decl {declVar = x, declClass = {{*** Exception: Too many outers
m1 = letrec (decl x (V x) (V x)) (V x)

[sweirich]

Ok, I think I've resolved the issue in my most recent commit. Now close doesn't give an error for negative levels (it just ignores them).