-- -*- haskell -*-
-- ghci -fglasgow-exts -fallow-undecidable-instances 
-- :load main.hs


    data H                         ;     data L = Khl H        -- Lattice
    eta :: s -> T l s              ;     eta e = T (\x -> e)   -- Monad injection
    newtype T l s = T (l -> s)     ;     t (T x) = x           -- T constructor/destructor
    
    class Bind l s2 where bind :: T l s1 -> (s1 -> s2) -> s2
    instance Bind l () where                                   -- P-Unit, LP-Unit
      bind m1 m2 = ()                                          
    instance (Bind l s1, Bind l s2) => Bind l (s1, s2) where   -- P-Pair, LP-Pair
      bind m1 m2 = (bind m1 (fst . m2), bind m1 (snd . m2))    
    instance (Bind l s2) => Bind l (s1 -> s2) where            -- P-Fun, LP-Fun
      bind m1 m2 = \x0 -> bind m1 (\x -> m2 x x0)                
    instance (Bind H s) => Bind H (T L s) where                -- P-Above, LP-Above with H </= L
      bind m1 m2 = T (\x0 -> bind m1 (\x -> t (m2 x) x0))     
    instance Bind H (T H s) where                              -- P-Under, LP-Under with H <= H
      bind (T m1) m2 = T (\x0 -> t (m2 (m1 x0)) x0)                  
    instance Bind L (T L s) where                              -- P-Under, LP-Under with L <= L
      bind (T m1) m2 = T (\x0 -> t (m2 (m1 x0)) x0)              
    instance Bind L (T H s) where                              -- P-Under, LP-Under with L <= H
      bind (T m1) m2 = T (\x0 -> t (m2 (m1 (Khl x0))) x0)        

    e :: T L Bool -> T H Bool
    e x1 = bind x1 (\x2 -> eta x2)

    -- e1 :: forall s l1 l. (Bind l (T l1 s)) => T l s -> T l1 s
    e1 x1 = bind x1 (\x2 -> eta x2)    

    -- This should not type check.
    -- e2 :: T H Bool -> T L Bool
    -- e2 x1 = bind x1 (\x2 -> eta x2)

    -- This requires type annotation because of monomorphic restriction.
    -- e3 = \x1 -> bind x1 (\x2 -> eta x2)