{- A not so practical, but impressive example. 

   To the reader: leave this example for last, and certainly after
   having read the closed version of type-safe casts. 

   This is Weirich's type-safe cast, made extensible. The way to achieve this
   is the following: In essence, all type-safe casts boil down to two
   nested typecase statements. So, in order to make a type-safe cast
   extensible we need to pass branches to the outer as well as the inner
   typecase. The details follow. -} 

{- Suppose that our basic type-safe cast operations are on integers
   and products  -}
let LTypeable = <lint,lproduct>;

{- A small Option library -} 
let Option_struct = \A:*.{ lJust of A | lNothing };
let nothing = \Ls:LABS.\B:*|Ls. (lNothing():(Option_struct B));
let some = \Ls:LABS.\B:*|Ls.\x:B. lJust(x):(Option_struct B);


let ecastHo = fix cast:[Ls:LABS].
                          [A:*|LTypeable ++ Ls, 
                           B:*|LTypeable ++ Ls, 
                           C:*->*|<*>]. 
                          {- outer branch type -} 
                          ([B:*|LTypeable++Ls, C:*->*|<*>].
                            (Ls => \A:*.(C A) -> (Option_struct (C B)) | LTypeable ++ Ls))
                          {- inner branch type -} 
                       -> ([A:*|LTypeable++Ls, C:*->*|<*>].
                            (Ls => \B:*.(C A) -> (Option_struct (C B)) | LTypeable ++ Ls))
                       -> (C A) -> (Option_struct (C B)). 

                {- abstract over the extension label set -} 
                 \Ls:LABS.\A:*|LTypeable++Ls.
                          \B:*|LTypeable++Ls.\C:*->*|<*>. 
                {- abstract over the outer branches -} 
                 \outer: [B:*|LTypeable++Ls, C:*->*|<*>].
                            (Ls => \A:*.(C A) -> (Option_struct (C B)) | LTypeable ++ Ls).
                {- abstract over the inner branches -} 
                 \inner: [A:*|LTypeable++Ls, C:*->*|<*>].
                            (Ls => \B:*.(C A) -> (Option_struct (C B)) | LTypeable ++ Ls).
                 (typecase A of { 
                       lint => (typecase B of {
                                  lint => \x:(C Int). some [<*>] [C Int] x
                                       : \B:*.(C Int) -> (Option_struct (C B))
                                       | LTypeable++Ls, 
                                  lproduct => \B1:*|LTypeable++Ls,
                                               B2:*|LTypeable++Ls. 
                                                 \x:(C Int). nothing [<*>] [C (B1*B2)]
                                           : \B:*.(C Int) -> (Option_struct (C B))
                                           | LTypeable++Ls
                                {- just as before, but add the inner branches here -}
                                } ++ inner [lint] [C] )
                                : \A:*. (C A) -> (Option_struct (C B))
                                | LTypeable++Ls, 
                        lproduct => \A1:*|LTypeable++Ls,
                                     A2:*|LTypeable++Ls.
                                     (typecase B of {
                                        lint => \x:C (A1*A2). nothing [<*>] [C Int]
                                             : \B:*.(C (A1*A2)) -> (Option_struct (C B))
                                             | LTypeable++Ls, 
                                        lproduct => \B1:*|LTypeable++Ls,
                                                     B2:*|LTypeable++Ls.                                       
                                                       let f = cast [Ls] [A1] [B1] [\D:*. C (D*A2)] outer inner in 
                                                       let g = cast [Ls] [A2] [B2] [\D:*. C (B1*D)] outer inner in
                                                       \x:C (A1*A2). 
                                                       match f x with
                                                         lNothing(_) -> nothing [<*>] [C (B1*B2)]
                                                       | lJust(y) -> begin
                                                                      match g y with 
                                                                        lNothing(_) -> nothing [<*>] [C (B1*B2)]
                                                                      | lJust(z) -> some [<*>] [C (B1*B2)] z
                                                                    end  
                                                 : \B:*.(C (A1*A2)) -> (Option_struct (C B))
                                                 | LTypeable++Ls
                                     {- just as before, but add the inner branches here -} 
                                     } ++ inner [A1*A2] [C] )
                                 : \A:*. (C A) -> (Option_struct (C B))
                                 | LTypeable++Ls
                    {- add the outer branches here -} 
                    } ++ outer [B] [C] );


{- Test the beast. 
   Suppose we want to extend type-safe cast with arrow types  -}
let Ls = <larrow>;


{- Inner has to fail---no types in the old labelset could mention arrow -} 
let inner = 
      \A:*|LTypeable++Ls, C:*->*|<*>. 
      { larrow => \B1:*|LTypeable++Ls, B2:*|LTypeable++Ls. 
                      \x:(C A). 
                        nothing [<*>] [C (B1 -> B2)]

               : \B:*.(C A) -> (Option_struct (C B))
               | LTypeable++Ls
      };

{- Outer is more complex, in particular it will have to do a typecase
   on B. The only case we will succeed is the diagonal case when also the 
   second type is an arrow type. In  all other cases we fail -} 
let outer = 
        fix outer: [B:*|LTypeable++Ls, C:*->*|<*>].
                     (Ls => \A:*.(C A) -> (Option_struct (C B)) | LTypeable ++ Ls). 
                   \B:*|LTypeable++Ls, C:*->*|<*>. 
        { larrow => \A1:*|LTypeable++Ls,A2:*|LTypeable++Ls.
                    typecase B of {

                       lint => \x:C (A1->A2). nothing [<*>] [C Int]
                            : \B:*.(C (A1->A2)) -> (Option_struct (C B))
                            | LTypeable++Ls, 

                       lproduct => \B1:*|LTypeable++Ls,
                                    B2:*|LTypeable++Ls.                                       
                                      \x:C (A1->A2). nothing [<*>] [C (B1*B2)]
                                : \B:*.(C (A1->A2)) -> (Option_struct (C B))
                                | LTypeable++Ls,

                       larrow => \B1:*|LTypeable++Ls,
                                  B2:*|LTypeable++Ls.
                                   let f = ecastHo [Ls] [A1] [B1] [\D:*. C (D->A2)] outer inner in 
                                   let g = ecastHo [Ls] [A2] [B2] [\D:*. C (B1->D)] outer inner in
                                   \x:C (A1->A2). 
                                      match f x with
                                        lNothing(_) -> 
                                                nothing [<*>] [C (B1->B2)]
                                      | lJust(y) -> begin
                                                        match g y with 
                                                        lNothing(_) -> nothing [<*>] [C (B1->B2)]
                                                        | lJust(z) -> some [<*>] [C (B1->B2)] z
                                                    end  
                                : \B:*.(C (A1->A2)) -> (Option_struct (C B))
                                | LTypeable++Ls
                    }
                : \A:*. (C A) -> (Option_struct (C B))
                | LTypeable++Ls 
        };

{- finally some small samples of calling these functions. remember
   that we pass the identity constructor as C to ecastHo  -} 
ecastHo [Ls] [Int*Int ] [Int*Int ] [\A:*.A] outer inner (2,3);
ecastHo [Ls] [Int -> Int ] [Int -> Int ] [\A:*.A] outer inner (\x:Int.3);
ecastHo [Ls] [Int -> Int ] [(Int*Int) -> Int ] [\A:*.A] outer inner (\x:Int.3)