{-# LANGUAGE UndecidableInstances #-}

-- | 'Syntactic' instance for functions for domains based on 'Typed' and
-- 'BindingT'

module Language.Syntactic.Sugar.BindingTyped where



import Data.Typeable

import Language.Syntactic
import Language.Syntactic.Functional



instance
    ( sym ~ Typed s
    , Syntactic a, Domain a ~ sym
    , Syntactic b, Domain b ~ sym
    , BindingT :<: s
    , Typeable (Internal a)
    , Typeable (Internal b)
    ) =>
      Syntactic (a -> b)
  where
    type Domain (a -> b)   = Domain a
    type Internal (a -> b) = Internal a -> Internal b
    desugar :: (a -> b) -> ASTF (Domain (a -> b)) (Internal (a -> b))
desugar a -> b
f = (ASTF (Typed s) (Internal a) -> ASTF (Typed s) (Internal b))
-> ASTF (Typed s) (Internal a -> Internal b)
forall (sym :: * -> *) (s :: * -> *) a b.
(sym ~ Typed s, BindingT :<: s, Typeable a, Typeable b) =>
(ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)
lamTyped (b -> ASTF (Typed s) (Internal b)
forall a. Syntactic a => a -> ASTF (Domain a) (Internal a)
desugar (b -> ASTF (Typed s) (Internal b))
-> (ASTF (Typed s) (Internal a) -> b)
-> ASTF (Typed s) (Internal a)
-> ASTF (Typed s) (Internal b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b)
-> (ASTF (Typed s) (Internal a) -> a)
-> ASTF (Typed s) (Internal a)
-> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ASTF (Typed s) (Internal a) -> a
forall a. Syntactic a => ASTF (Domain a) (Internal a) -> a
sugar)
    sugar :: ASTF (Domain (a -> b)) (Internal (a -> b)) -> a -> b
sugar     = [Char] -> ASTF (Typed s) (Internal a -> Internal b) -> a -> b
forall a. HasCallStack => [Char] -> a
error [Char]
"sugar not implemented for (a -> b)"