{- The Extensible Equality Example from the paper -} 

{- Li contains integers/booleans  -} 
let Li = <lint,lbool>;

{- First, abstract over the labelset of the extension Ls -} 
let eq = \Ls:LABS.
  {- Take the xtension as an argument -} 
  \y:Ls => \A:*.A->A->Bool | Ls ++ Li.
     fix eq:[A:*|Ls++Li].A->A->Bool. 
        {- abstract over a type that can contain labels in Li++Ls and
           analyze it. Call y when the constructor is not in Li -} 
        \A:*|Li++Ls.typecase A of (y ++ {lint => \x:Int,y:Int. x = y
                    {- ignore the rest, annotations to make the 
                       typechecker happy: the type scheme and the label 
                       set of the types mentioned in the branch. -} 
                                              : \A:*.A->A->Bool
                                              | Ls ++ Li, 
                                         lbool => \x:Bool,y:Bool.
                                            if x then y else (not y)
                                               : \A:*.A->A->Bool
                                               | Ls++Li
                                         });

{- Extension for products -} 
let prod_ext = 
  fix prod_ext:<lproduct> => \A:*.A->A->Bool | Li++<lproduct>. 
        { {- lproduct : * -> * -> *, so we need to abstract over 
             two type variables of kind * first. 
           -} 
          lproduct => \A:*|Li++<lproduct>. 
                      \B:*|Li++<lproduct>. 
                       {- then take the actual term arguments -} 
                        \x:A*B,y:A*B. 
                            (eq [<lproduct>] prod_ext [A] x.fst y.fst) &&
                            (eq [<lproduct>] prod_ext [B] x.snd y.snd) 
                   : \A:*.A->A->Bool 
                   | Li++<lproduct>
        };
                        
{- Call Site, simply call eq with the extension -} 
eq [<lproduct>] prod_ext [Int*Bool] (1,true) (1,true)