Language/Symantic/Expr/From.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE DefaultSignatures #-}
   4 {-# LANGUAGE FlexibleContexts #-}
   5 {-# LANGUAGE FlexibleInstances #-}
   6 {-# LANGUAGE GADTs #-}
   7 {-# LANGUAGE KindSignatures #-}
   8 {-# LANGUAGE MultiParamTypeClasses #-}
   9 {-# LANGUAGE OverloadedStrings #-}
  10 {-# LANGUAGE Rank2Types #-}
  11 {-# LANGUAGE ScopedTypeVariables #-}
  12 {-# LANGUAGE TypeFamilies #-}
  13 {-# LANGUAGE TypeOperators #-}
  14 {-# LANGUAGE UndecidableInstances #-}
  15 module Language.Symantic.Expr.From where
  16
  17 import Data.Maybe (fromMaybe)
  18 import Data.Monoid
  19 import Data.Proxy (Proxy(..))
  20 import Data.Text (Text)
  21 import qualified Data.Text as Text
  22 import Data.Type.Equality ((:~:)(Refl))
  23 import GHC.Prim (Constraint)
  24
  25 import Language.Symantic.Type
  26 import Language.Symantic.Expr.Root
  27 import Language.Symantic.Expr.Alt
  28 import Language.Symantic.Expr.Error
  29 import Language.Symantic.Trans.Common
  30 import Language.Symantic.Repr
  31
  32 -- * Class 'Expr_From'
  33 -- | Parse given @ast@ into
  34 -- a 'Type_Root_of_Expr' and
  35 -- a 'Forall_Repr_with_Context',
  36 -- or return an 'Error_of_Expr'.
  37 class Expr_From ast (ex:: *) where
  38         expr_from :: ExprFrom ast ex hs ret
  39 instance -- Expr_From
  40  ( Expr_From ast (ex (Expr_Root ex))
  41  , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
  42  ) => Expr_From ast (Expr_Root ex) where
  43         expr_from _ex ctx ast k =
  44                 expr_from (Proxy::Proxy (ex (Expr_Root ex)))
  45                  ctx ast $ \ty (Forall_Repr_with_Context repr) ->
  46                 k ty (Forall_Repr_with_Context repr)
  47 instance -- Expr_From
  48  ( Expr_From ast (curr root)
  49  , Expr_From ast (next root)
  50  , Root_of_Expr (curr root) ~ root
  51  , Root_of_Expr (next root) ~ root
  52  , Error_Expr_Unlift (Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
  53                                  (Type_Root_of_Expr root) ast)
  54                      (Error_of_Expr ast root)
  55  ) => Expr_From ast (Expr_Alt curr next root) where
  56         expr_from _ex ctx ast k =
  57                 case expr_from (Proxy::Proxy (curr root)) ctx ast $
  58                  \ty (Forall_Repr_with_Context repr) ->
  59                         Right $ k ty (Forall_Repr_with_Context repr) of
  60                  Right ret -> ret
  61                  Left err ->
  62                         case error_expr_unlift err of
  63                          Just (Error_Expr_Unsupported_here _
  64                           :: Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
  65                                         (Type_Root_of_Expr root) ast) ->
  66                                 expr_from (Proxy::Proxy (next root)) ctx ast $
  67                                  \ty (Forall_Repr_with_Context repr) ->
  68                                 k ty (Forall_Repr_with_Context repr)
  69                          _ -> Left err
  70
  71 -- ** Type 'ExprFrom'
  72 -- | Convenient type synonym defining a parser.
  73 type ExprFrom ast ex hs ret
  74  = Proxy ex
  75  -- ^ Select the 'Expr_From' instance.
  76  -> ast
  77  -- ^ The input data to parse.
  78  -> Lambda_Context (Lambda_Var (Type_Root_of_Expr ex)) hs
  79  -- ^ The bound variables in scope and their types:
  80  -- built top-down in the heterogeneous list @hs@,
  81  -- from the closest including lambda abstraction to the farest.
  82  -> ( forall h
  83     .  Type_Root_of_Expr ex h
  84     -> Forall_Repr_with_Context ex hs h
  85     -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret )
  86  -- ^ The accumulating continuation called bottom-up.
  87  -> Either (Error_of_Expr ast (Root_of_Expr ex)) ret
  88
  89 -- ** Type 'Lambda_Context'
  90 -- | GADT for a typing context,
  91 -- accumulating an @item@ at each lambda;
  92 -- used to accumulate object-types (in 'Expr_From')
  93 -- or host-terms (in 'Repr_Host')
  94 -- associated with the 'Lambda_Var's in scope.
  95 data Lambda_Context :: (* -> *) -> [*] -> * where
  96         Lambda_Context_Empty :: Lambda_Context item '[]
  97         Lambda_Context_Next  :: item h
  98                              -> Lambda_Context item hs
  99                              -> Lambda_Context item (h ': hs)
 100 infixr 5 `Lambda_Context_Next`
 101
 102 -- ** Type 'Lambda_Var'
 103 -- | Join a name and a type.
 104 --
 105 -- This data type is used to handle lambda variables by name
 106 -- (instead of DeBruijn indices for instance).
 107 data Lambda_Var ty h
 108  =   Lambda_Var Lambda_Var_Name (ty h)
 109 type Lambda_Var_Name = Text
 110
 111 -- ** Type 'Forall_Repr_with_Context'
 112 -- | A data type embedding a universal quantification
 113 -- over an interpreter @repr@
 114 -- and qualified by the symantics of an expression.
 115 --
 116 -- Moreover the expression is abstracted by a 'Lambda_Context'
 117 -- built top-down at parsing time
 118 -- to build a /Higher-Order Abstract Syntax/ (HOAS)
 119 -- for lambda abstractions.
 120 --
 121 -- This data type is used to keep a parsed expression polymorphic enough
 122 -- to stay interpretable by different interpreters.
 123 --
 124 -- NOTE: 'Sym_of_Expr'@ ex repr@
 125 -- is needed to be able to use symantic methods of the parsed expression
 126 -- into a 'Forall_Repr_with_Context'@ ex@.
 127 --
 128 -- NOTE: 'Sym_of_Expr'@ (@'Root_of_Expr'@ ex) repr@
 129 -- is needed to be able to use an expression
 130 -- out of a 'Forall_Repr_with_Context'@ (@'Root_of_Expr'@ ex)@
 131 -- into a 'Forall_Repr_with_Context'@ ex@,
 132 -- which happens when a symantic method includes a polymorphic type
 133 -- and thus calls: 'expr_from'@ (Proxy::Proxy (@'Root_of_Expr'@ ex))@.
 134 --
 135 -- NOTE: 'Sym_Lambda_Lam'@ repr@
 136 -- is needed to be able to parse partially applied functions
 137 -- (when their type is knowable).
 138 data Forall_Repr_with_Context ex hs h
 139  =   Forall_Repr_with_Context
 140  (   forall repr. ( Sym_of_Expr ex repr
 141                   , Sym_of_Expr (Root_of_Expr ex) repr
 142                   , Sym_Lambda_Lam repr
 143                   ) => Lambda_Context repr hs -> repr h )
 144
 145 -- ** Type 'Forall_Repr'
 146 -- | 'Forall_Repr_with_Context' applied on a 'Lambda_Context'.
 147 data Forall_Repr ex h
 148  =   Forall_Repr
 149  { unForall_Repr :: forall repr
 150                  .  ( Sym_of_Expr ex repr
 151                     , Sym_of_Expr (Root_of_Expr ex) repr
 152                     , Sym_Lambda_Lam repr )
 153                  => repr h }
 154
 155 -- ** Class 'Sym_Lambda_Lam'
 156 class Sym_Lambda_Lam repr where
 157         -- | /Lambda abstraction/.
 158         lam :: (repr arg -> repr res) -> repr ((->) arg res)
 159         default lam :: Trans t repr
 160          => (t repr arg -> t repr res) -> t repr ((->) arg res)
 161         lam f = trans_lift $ lam $ trans_apply . f . trans_lift
 162 instance Sym_Lambda_Lam Repr_Host where
 163         lam f = Repr_Host (unRepr_Host . f . Repr_Host)
 164 instance Sym_Lambda_Lam Repr_Text where
 165         lam f = Repr_Text $ \p v ->
 166                 let p' = Precedence 1 in
 167                 let x = "x" <> Text.pack (show v) in
 168                 paren p p' $ "\\" <> x <> " -> "
 169                  <> unRepr_Text (f (Repr_Text $ \_p _v -> x)) p' (succ v)
 170 instance (Sym_Lambda_Lam r1, Sym_Lambda_Lam r2) => Sym_Lambda_Lam (Repr_Dup r1 r2) where
 171         lam f = let lam_f = lam f in repr_dup_1 lam_f `Repr_Dup` repr_dup_2 lam_f
 172
 173 -- ** Type family 'Sym_of_Expr'
 174 -- | The symantic of an expression.
 175 type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint
 176 type instance Sym_of_Expr (Expr_Root ex) repr
 177  =            Sym_of_Expr (ex (Expr_Root ex)) repr
 178 type instance Sym_of_Expr (Expr_Alt curr next root) repr
 179  = ( Sym_of_Expr (curr root) repr
 180    , Sym_of_Expr (next root) repr
 181    )
 182
 183 -- * Checks
 184
 185 -- | Parsing utility to check that the type resulting
 186 -- from the application of a given type family to a given type
 187 -- is within the type stack,
 188 -- or raise 'Error_Expr_Type_mismatch'.
 189 check_type0_family
 190  :: forall ast ex tf root ty h ret.
 191  ( root ~ Root_of_Expr ex
 192  , ty ~ Type_Root_of_Expr ex
 193  , Type0_Family tf ty
 194  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 195                    (Error_of_Expr ast root)
 196  ) => Proxy tf -> Proxy ex -> ast -> ty h
 197  -> (ty (Host_of_Type0_Family tf h) -> Either (Error_of_Expr ast root) ret)
 198  -> Either (Error_of_Expr ast root) ret
 199 check_type0_family tf ex ast ty k =
 200         case type0_family tf ty of
 201          Just t -> k t
 202          Nothing -> Left $ error_expr ex $
 203                 Error_Expr_Type (error_type_lift $ Error_Type_No_Type_Family ast) ast
 204
 205 -- | Parsing utility to check that two types are equal,
 206 -- or raise 'Error_Expr_Type_mismatch'.
 207 check_type0_eq
 208  :: forall ast ex root ty x y ret.
 209  ( root ~ Root_of_Expr ex
 210  , ty ~ Type_Root_of_Expr ex
 211  , Type0_Eq ty
 212  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 213                    (Error_of_Expr ast root)
 214  ) => Proxy ex -> ast -> ty x -> ty y
 215  -> (x :~: y -> Either (Error_of_Expr ast root) ret)
 216  -> Either (Error_of_Expr ast root) ret
 217 check_type0_eq ex ast x y k =
 218         case x `type0_eq` y of
 219          Just Refl -> k Refl
 220          Nothing -> Left $ error_expr ex $
 221                 Error_Expr_Type_mismatch ast
 222                  (Exists_Type0 x)
 223                  (Exists_Type0 y)
 224
 225 -- | Parsing utility to check that two 'Type1' are equal,
 226 -- or raise 'Error_Expr_Type_mismatch'.
 227 check_type1_eq
 228  :: forall ast ex root ty h1 h2 a1 a2 ret.
 229  ( root ~ Root_of_Expr ex
 230  , ty ~ Type_Root_of_Expr ex
 231  , Type1_Eq ty
 232  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 233                    (Error_of_Expr ast root)
 234  )
 235  => Proxy ex -> ast -> ty (h1 a1) -> ty (h2 a2)
 236  -> (h1 :~: h2 -> Either (Error_of_Expr ast root) ret)
 237  -> Either (Error_of_Expr ast root) ret
 238 check_type1_eq ex ast h1 h2 k =
 239         case h1 `type1_eq` h2 of
 240          Just Refl -> k Refl
 241          Nothing -> Left $ error_expr ex $
 242                 Error_Expr_Type_mismatch ast
 243                  (Exists_Type0 h1)
 244                  (Exists_Type0 h2)
 245
 246 -- | Parsing utility to check that a 'Type0' or higher
 247 -- is an instance of a given 'Constraint',
 248 -- or raise 'Error_Expr_Constraint_missing'.
 249 check_type0_constraint
 250  :: forall ast ex c root ty h ret.
 251  ( root ~ Root_of_Expr ex
 252  , ty ~ Type_Root_of_Expr ex
 253  , Type0_Constraint c ty
 254  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 255                    (Error_of_Expr ast root)
 256  )
 257  => Proxy ex -> Proxy c -> ast -> ty h
 258  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 259  -> Either (Error_of_Expr ast root) ret
 260 check_type0_constraint ex c ast ty k =
 261         case type0_constraint c ty of
 262          Just Dict -> k Dict
 263          Nothing -> Left $ error_expr ex $
 264                 Error_Expr_Constraint_missing ast
 265                  {-(Exists_Dict c)-}
 266                  -- FIXME: not easy to report the constraint
 267                  -- and still support 'Eq' and 'Show' deriving.
 268                  (Exists_Type0 ty)
 269
 270 -- | Parsing utility to check that a 'Type1' or higher
 271 -- is an instance of a given 'Constraint',
 272 -- or raise 'Error_Expr_Constraint_missing'.
 273 check_type1_constraint
 274  :: forall ast ex c root ty h a ret.
 275  ( root ~ Root_of_Expr ex
 276  , ty ~ Type_Root_of_Expr ex
 277  , Type1_Constraint c ty
 278  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 279                    (Error_of_Expr ast root)
 280  ) => Proxy ex -> Proxy c -> ast -> ty (h a)
 281  -> (Dict (c h) -> Either (Error_of_Expr ast root) ret)
 282  -> Either (Error_of_Expr ast root) ret
 283 check_type1_constraint ex c ast ty k =
 284         case type1_constraint c ty of
 285          Just Dict -> k Dict
 286          Nothing -> Left $ error_expr ex $
 287                 Error_Expr_Constraint_missing ast
 288                  (Exists_Type0 ty)
 289
 290 -- | Parsing utility to check that the given type is at least a 'Type1'
 291 -- or raise 'Error_Expr_Type_mismatch'.
 292 check_type1
 293  :: forall ast ex root ty h ret.
 294  ( root ~ Root_of_Expr ex
 295  , ty ~ Type_Root_of_Expr ex
 296  , Type1_Unlift (Type_of_Expr root)
 297  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 298                    (Error_of_Expr ast root)
 299  ) => Proxy ex -> ast -> ty h
 300  -> (forall (t1:: *).
 301      ( Type1 t1 ty h
 302      , Type1_Lift t1 ty (Type_Var0 :|: Type_Var1 :|: Type_of_Expr root)
 303      ) -> Either (Error_of_Expr ast root) ret)
 304  -> Either (Error_of_Expr ast root) ret
 305 check_type1 ex ast ty k =
 306         (`fromMaybe` type1_unlift (unType_Root ty) (Just . k)) $
 307         Left $ error_expr ex $
 308         Error_Expr_Type_mismatch ast
 309          (Exists_Type0 (type_var1 SZero (type_var0 SZero)
 310          :: ty (Var1 Var0)))
 311          (Exists_Type0 ty)
 312
 313 -- * Parsers
 314
 315 -- | Like 'expr_from' but for a root expression.
 316 root_expr_from
 317  :: forall ast root.
 318  ( Expr_From ast root
 319  , Root_of_Expr root ~ root
 320  ) => Proxy root -> ast
 321  -> Either (Error_of_Expr ast root)
 322            (Exists_Type0_and_Repr (Type_Root_of_Expr root)
 323                                   (Forall_Repr root))
 324 root_expr_from _ex ast =
 325         expr_from (Proxy::Proxy root) ast
 326          Lambda_Context_Empty $ \ty (Forall_Repr_with_Context repr) ->
 327         Right $ Exists_Type0_and_Repr ty $
 328                 Forall_Repr $ repr Lambda_Context_Empty
 329
 330 -- | Parse a literal.
 331 lit_from
 332  :: forall ty lit ex ast hs ret.
 333  ( ty ~ Type_Root_of_Expr ex
 334  , Read lit
 335  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 336                    (Error_of_Expr ast (Root_of_Expr ex))
 337  ) => (forall repr. Sym_of_Expr ex repr => lit -> repr lit)
 338  -> ty lit -> Text
 339  -> ExprFrom ast ex hs ret
 340 lit_from lit ty_lit toread ex ast _ctx k =
 341         case read_safe toread of
 342          Left err -> Left $ error_expr ex $ Error_Expr_Read err ast
 343          Right (i::lit) -> k ty_lit $ Forall_Repr_with_Context $ const $ lit i
 344
 345 -- | Parse a unary class operator.
 346 class_op1_from
 347  :: forall root ty cl ex ast hs ret.
 348  ( ty ~ Type_Root_of_Expr ex
 349  , root ~ Root_of_Expr ex
 350  , Type0_Eq ty
 351  , Expr_From ast root
 352  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 353                    (Error_of_Expr ast root)
 354  , Root_of_Expr root ~ root
 355  , Type0_Constraint cl ty
 356  ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit)
 357  -> Proxy cl -> ast
 358  -> ExprFrom ast ex hs ret
 359 class_op1_from op cl ast_x ex _ast ctx k =
 360         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 361         check_type0_constraint ex cl ast_x ty_x $ \Dict ->
 362         k ty_x $ Forall_Repr_with_Context (op . x)
 363
 364 -- | Parse a binary class operator.
 365 class_op2_from
 366  :: forall root ty cl ex ast hs ret.
 367  ( ty ~ Type_Root_of_Expr ex
 368  , root ~ Root_of_Expr ex
 369  , Type0_Eq ty
 370  , Expr_From ast root
 371  , Type0_Constraint cl ty
 372  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 373                    (Error_of_Expr ast root)
 374  , Root_of_Expr root ~ root
 375  ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
 376  -> Proxy cl -> ast -> ast
 377  -> ExprFrom ast ex hs ret
 378 class_op2_from op cl ast_x ast_y ex ast ctx k =
 379         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 380         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
 381         check_type0_constraint ex cl ast_x ty_x $ \Dict ->
 382         check_type0_constraint ex cl ast_y ty_y $ \Dict ->
 383         check_type0_eq ex ast ty_x ty_y $ \Refl ->
 384         k ty_x $ Forall_Repr_with_Context $
 385          \c -> x c `op` y c
 386
 387 -- | Parse a binary class operator, partially applied.
 388 class_op2_from1
 389  :: forall root ty cl ex ast hs ret.
 390  ( ty ~ Type_Root_of_Expr ex
 391  , root ~ Root_of_Expr ex
 392  , Type0_Eq ty
 393  , Type0_Constraint cl ty
 394  , Type0_Lift Type_Fun (Type_of_Expr root)
 395  , Expr_From ast root
 396  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 397                    (Error_of_Expr ast root)
 398  , Root_of_Expr root ~ root
 399  ) => (forall lit repr. (cl lit, Sym_of_Expr ex repr) => repr lit -> repr lit -> repr lit)
 400  -> Proxy cl -> ast
 401  -> ExprFrom ast ex hs ret
 402 class_op2_from1 op cl ast_x ex _ast ctx k =
 403         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 404         check_type0_constraint ex cl ast_x ty_x $ \Dict ->
 405         k (type_fun ty_x ty_x) $ Forall_Repr_with_Context $
 406          \c -> lam $ \y -> x c `op` y
 407
 408 -- | Parse a unary operator.
 409 op1_from
 410  :: forall root ty lit ex ast hs ret.
 411  ( ty ~ Type_Root_of_Expr ex
 412  , root ~ Root_of_Expr ex
 413  , Type0_Eq ty
 414  , Expr_From ast root
 415  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 416                    (Error_of_Expr ast root)
 417  , Root_of_Expr root ~ root
 418  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
 419  -> ty lit -> ast
 420  -> ExprFrom ast ex hs ret
 421 op1_from op ty_lit ast_x ex ast ctx k =
 422         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 423         check_type0_eq ex ast ty_lit ty_x $ \Refl ->
 424         k ty_x $ Forall_Repr_with_Context (op . x)
 425
 426 -- | Parse a unary operator, partially applied.
 427 op1_from0
 428  :: forall root ty lit ex ast hs ret.
 429  ( ty ~ Type_Root_of_Expr ex
 430  , root ~ Root_of_Expr ex
 431  , Type0_Eq ty
 432  , Type0_Lift Type_Fun (Type_of_Expr root)
 433  , Expr_From ast root
 434  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 435                    (Error_of_Expr ast root)
 436  , Root_of_Expr root ~ root
 437  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit)
 438  -> ty lit
 439  -> ExprFrom ast ex hs ret
 440 op1_from0 op ty_lit _ex _ast _ctx k =
 441         k (type_fun ty_lit ty_lit) $ Forall_Repr_with_Context $
 442          \_c -> lam op
 443
 444 -- | Parse a binary operator.
 445 op2_from
 446  :: forall root ty lit ex ast hs ret.
 447  ( ty ~ Type_Root_of_Expr ex
 448  , root ~ Root_of_Expr ex
 449  , Type0_Eq ty
 450  , Expr_From ast root
 451  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 452                    (Error_of_Expr ast root)
 453  , Root_of_Expr root ~ root
 454  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 455  -> ty lit -> ast -> ast
 456  -> ExprFrom ast ex hs ret
 457 op2_from op ty_lit ast_x ast_y ex ast ctx k =
 458         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 459         expr_from (Proxy::Proxy root) ast_y ctx $ \ty_y (Forall_Repr_with_Context y) ->
 460         check_type0_eq ex ast ty_lit ty_x $ \Refl ->
 461         check_type0_eq ex ast ty_lit ty_y $ \Refl ->
 462         k ty_x $ Forall_Repr_with_Context $
 463          \c -> x c `op` y c
 464
 465 -- | Parse a binary operator, partially applied.
 466 op2_from1
 467  :: forall root ty lit ex ast hs ret.
 468  ( ty ~ Type_Root_of_Expr ex
 469  , root ~ Root_of_Expr ex
 470  , Type0_Eq ty
 471  , Type0_Lift Type_Fun (Type_of_Expr root)
 472  , Expr_From ast root
 473  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 474                    (Error_of_Expr ast root)
 475  , Root_of_Expr root ~ root
 476  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 477  -> ty lit -> ast
 478  -> ExprFrom ast ex hs ret
 479 op2_from1 op ty_lit ast_x ex ast ctx k =
 480         expr_from (Proxy::Proxy root) ast_x ctx $ \ty_x (Forall_Repr_with_Context x) ->
 481         check_type0_eq ex ast ty_lit ty_x $ \Refl ->
 482                 k (type_fun ty_x ty_x) $ Forall_Repr_with_Context $
 483                  \c -> lam $ \y -> x c `op` y
 484
 485 -- | Parse a binary operator, partially applied.
 486 op2_from0
 487  :: forall root ty lit ex ast hs ret.
 488  ( ty ~ Type_Root_of_Expr ex
 489  , root ~ Root_of_Expr ex
 490  , Type0_Eq ty
 491  , Type0_Lift Type_Fun (Type_of_Expr root)
 492  , Expr_From ast root
 493  , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
 494                    (Error_of_Expr ast root)
 495  , Root_of_Expr root ~ root
 496  ) => (forall repr. Sym_of_Expr ex repr => repr lit -> repr lit -> repr lit)
 497  -> ty lit
 498  -> ExprFrom ast ex hs ret
 499 op2_from0 op ty_lit _ex _ast _ctx k =
 500         k (type_fun ty_lit $ type_fun ty_lit ty_lit) $ Forall_Repr_with_Context $
 501          \_c -> lam $ \x -> lam $ \y -> x `op` y