+-- Lastly, you can wrap code-brackets around an identifier in a
+-- top-level, let, or where binding. Notice how GHC doesn't complain
+-- here about defining an identifier twice!
+
+foo = \x -> x+1
+<[ foo ]> = <[ \(x::Bool) -> x ]>
+
+-- Now you can use foo (the second one!) inside code-brackets:
+
+bar x = <[ foo ~~x ]>
+
+bar :: forall g. <[Bool]>@g -> <[Bool]>@g
+
+-- In fact, the identifiers have completely unrelated types. Which
+-- brings up another important point: types are ALWAYS assigned
+-- "relative to" depth zero. So although we imagine "foo" existing at
+-- depth-one, its type is quite firmly established as <[ Bool -> Bool ]>
+
+-- It has to be this way -- to see why, consider a term which is more
+-- polymorphic than "foo":
+
+<[ foo' ]> = <[ \x -> x ]>
+
+-- Its type is:
+
+<[ foo' ]> :: forall a g . <[ a -> a ]>@g
+
+-- ...and there's no way to express the g-polymorphism entirely from
+-- within the brackets.
+
+-- So why does all of this matter? Mainly so that we can continue to use . We'd like
+-- the "+" operator to work "as expected" -- in other words, we'd like
+-- people to be able to write things like
+
+increment_at_level1 = <[ \x -> x + 1 ]>
+
+-- However, in unmodified haskell an identifier like (+) may have only
+-- one type. In this case that type is:
+--
+-- (+) :: Num a => a -> a -> a
+--
+-- Now, we could simply decree that when (+) appears inside code
+-- brackets, an "implicit ~~" is inserted, so the desugared expression
+-- is:
+--
+-- increment_at_level1 = <[ \x -> ~~(+) x 1 ]>
+--
+-- unfortunately this isn't going to work for guest languages that
+-- don't have higher-order functions. Haskell uses curried arguments
+-- because it has higher-order functions, but in a first-order guest
+-- language a more sensible type for (+) would be:
+--
+-- (+) :: Num a => (a,a) -> a
+--
+-- ... or even something less polymorphic, like
+--
+-- (+) :: (Int,Int) -> Int
+--
+-- so to maintain flexibility, we allow an identifier to have
+-- different types at different syntactic depths; this way type
+-- choices made for Haskell don't get imposed on guest languages that
+-- are missing some of its features.
+--
+-- In hindsight, what we REALLY want is for increment_at_level1 to
+-- be desugared like this (much like the Arrow (|...|) syntax):
+--
+-- increment_at_level1 = <[ \x -> ~~( <[x]> + <[1]> ) ]>
+--
+-- ... because then we can declare
+--
+-- instance Num a => Num <[a]> where ...
+--
+-- or just
+--
+-- instance Num <[Int]> where ...
+--
+-- unfortunately there's a major problem: knowing how to do this sort
+-- of desugaring requires knowing the *arity* of a function. For
+-- symbols we can kludge it by checking Haskell's parsing rules (there
+-- are only a handful of unary symbols; all others are binary), but
+-- this is crude and won't work at all for non-symbol identifiers.
+-- And we can look at a type like x->y->z and say "oh, that's a
+-- two-argument function", but sometimes GHC doesn't know the complete
+-- type of an identifier in the midst of unification (i.e. "x has type
+-- Int->a for some a, where a could be Int or Int->Int"), so guessing
+-- the arity from the type cannot be done during parsing, which is
+-- when we need to do this.
+--
+-- Okay, I think that's more or less a brain dump of why I changed the
+-- scoping rules and the problems with the other solutions I tried.
+--
+-- I am very interested in hearing any suggestions on better ways of
+-- dealing with this, so long as you can still use operators like (+)
+-- in guest languages without higher-order functions.
+--
+
+
+
+
+
+
+-- The rest of this file contains a bunch of example programs: