    {-# Language ImplicitParams #-}
    {-# Language FlexibleInstances #-}
    {-# Language RecursiveDo #-}
    {-# Language BlockArguments #-}
    {-# Language RankNTypes #-}
    {-# Language OverloadedStrings #-}
    module Cryptol.TypeCheck.ModuleBacktickInstance
      ( MBQual
      , doBacktickInstance
      ) where

    import Data.Set(Set)
    import qualified Data.Set as Set
    import Data.Map(Map)
    import qualified Data.Map as Map
    import MonadLib
    import Data.List(group,sort)
    import Data.Maybe(mapMaybe)
    import qualified Data.Text as Text

    import Cryptol.Utils.Ident(ModPath(..), modPathIsOrContains,Namespace(..)
                              , Ident, mkIdent, identText
                              , ModName, modNameChunksText )
    import Cryptol.Utils.PP(pp)
    import Cryptol.Utils.Panic(panic)
    import Cryptol.Utils.RecordMap(RecordMap,recordFromFields,recordFromFieldsErr)
    import Cryptol.Parser.Position
    import Cryptol.ModuleSystem.Name(
      nameModPath, nameModPathMaybe, nameIdent, mapNameIdent)
    import Cryptol.TypeCheck.AST
    import Cryptol.TypeCheck.Error
    import qualified Cryptol.TypeCheck.Monad as TC

    type MBQual a = (Maybe ModName, a)

    {- | Rewrite declarations to add the given module parameters.
    Assumes the renaming due to the instantiation has already happened.
    The module being rewritten should not contain any nested functors
    (or module with only top-level constraints) because it is not clear
    how to parameterize the parameters.
    -}
    doBacktickInstance ::
      Set (MBQual TParam) ->
      [Prop] ->
      Map (MBQual Name) Type ->
      ModuleG (Located (ImpName Name)) ->
      TC.InferM (ModuleG (Located (ImpName Name)))
    doBacktickInstance :: Set (MBQual TParam)
    -> [Prop]
    -> Map (MBQual Name) Prop
    -> ModuleG (Located (ImpName Name))
    -> InferM (ModuleG (Located (ImpName Name)))
    doBacktickInstance Set (MBQual TParam)
    as [Prop]
    ps Map (MBQual Name) Prop
    mp ModuleG (Located (ImpName Name))
    m
      | Set (MBQual TParam) -> Bool
    forall a. Set a -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null Set (MBQual TParam)
    as Bool -> Bool -> Bool
    && [Prop] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Prop]
    ps Bool -> Bool -> Bool
    && Map (MBQual Name) Prop -> Bool
    forall k a. Map k a -> Bool
    Map.null Map (MBQual Name) Prop
    mp = ModuleG (Located (ImpName Name))
    -> InferM (ModuleG (Located (ImpName Name)))
    forall a. a -> InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModuleG (Located (ImpName Name))
    m
      | Bool
    otherwise =
        RO
    -> ReaderT RO InferM (ModuleG (Located (ImpName Name)))
    -> InferM (ModuleG (Located (ImpName Name)))
    forall i (m :: * -> *) a. i -> ReaderT i m a -> m a
    runReaderT
          RO { isOurs :: Name -> Bool
    isOurs = \Name
    x -> case Name -> Maybe ModPath
    nameModPathMaybe Name
    x of
                                Maybe ModPath
    Nothing -> Bool
    False
                                Just ModPath
    y  -> ModPath
    ourPath ModPath -> ModPath -> Bool
    `modPathIsOrContains` ModPath
    y
             , tparams :: [MBQual TParam]
    tparams = Set (MBQual TParam) -> [MBQual TParam]
    forall a. Set a -> [a]
    Set.toList Set (MBQual TParam)
    as
             , constraints :: [Prop]
    constraints = [Prop]
    ps
             , vparams :: Map (MBQual Name) Prop
    vparams = Map (MBQual Name) Prop
    mp
             , newNewtypes :: Map Name Newtype
    newNewtypes = Map Name Newtype
    forall k a. Map k a
    Map.empty
             }

        do Bool -> ReaderT RO InferM () -> ReaderT RO InferM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([(BIWhat, Name)] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [(BIWhat, Name)]
    bad)
                  (Error -> ReaderT RO InferM ()
    recordError (BadBacktickInstance -> Error
    FunctorInstanceBadBacktick ([(BIWhat, Name)] -> BadBacktickInstance
    BINested [(BIWhat, Name)]
    bad)))

           rec
             Map Name TySyn
    ts <- Map Name Newtype
    -> (ModuleG (Located (ImpName Name)) -> Map Name TySyn)
    -> ReaderT RO InferM (Map Name TySyn)
    forall {a}.
    AddParams a =>
    Map Name Newtype
    -> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
    doAddParams Map Name Newtype
    nt ModuleG (Located (ImpName Name)) -> Map Name TySyn
    forall mname. ModuleG mname -> Map Name TySyn
    mTySyns
             Map Name Newtype
    nt <- Map Name Newtype
    -> (ModuleG (Located (ImpName Name)) -> Map Name Newtype)
    -> ReaderT RO InferM (Map Name Newtype)
    forall {a}.
    AddParams a =>
    Map Name Newtype
    -> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
    doAddParams Map Name Newtype
    nt ModuleG (Located (ImpName Name)) -> Map Name Newtype
    forall mname. ModuleG mname -> Map Name Newtype
    mNewtypes
             [DeclGroup]
    ds <- Map Name Newtype
    -> (ModuleG (Located (ImpName Name)) -> [DeclGroup])
    -> ReaderT RO InferM [DeclGroup]
    forall {a}.
    AddParams a =>
    Map Name Newtype
    -> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
    doAddParams Map Name Newtype
    nt ModuleG (Located (ImpName Name)) -> [DeclGroup]
    forall mname. ModuleG mname -> [DeclGroup]
    mDecls

           ModuleG (Located (ImpName Name))
    -> ReaderT RO InferM (ModuleG (Located (ImpName Name)))
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ModuleG (Located (ImpName Name))
    m
             { mTySyns :: Map Name TySyn
    mTySyns   = Map Name TySyn
    ts
             , mNewtypes :: Map Name Newtype
    mNewtypes = Map Name Newtype
    nt
             , mDecls :: [DeclGroup]
    mDecls    = [DeclGroup]
    ds
             }

        where
        bad :: [(BIWhat, Name)]
    bad = (ModuleG (Located (ImpName Name)) -> Map Name (ModuleG Name))
    -> BIWhat -> [(BIWhat, Name)]
    forall {b} {a} {a}.
    (ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
    mkBad ModuleG (Located (ImpName Name)) -> Map Name (ModuleG Name)
    forall mname. ModuleG mname -> Map Name (ModuleG Name)
    mFunctors BIWhat
    BIFunctor
           [(BIWhat, Name)] -> [(BIWhat, Name)] -> [(BIWhat, Name)]
    forall a. [a] -> [a] -> [a]
    ++ (ModuleG (Located (ImpName Name)) -> Map Name AbstractType)
    -> BIWhat -> [(BIWhat, Name)]
    forall {b} {a} {a}.
    (ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
    mkBad ModuleG (Located (ImpName Name)) -> Map Name AbstractType
    forall mname. ModuleG mname -> Map Name AbstractType
    mPrimTypes BIWhat
    BIAbstractType
           [(BIWhat, Name)] -> [(BIWhat, Name)] -> [(BIWhat, Name)]
    forall a. [a] -> [a] -> [a]
    ++ (ModuleG (Located (ImpName Name)) -> Map Name ModParamNames)
    -> BIWhat -> [(BIWhat, Name)]
    forall {b} {a} {a}.
    (ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
    mkBad ModuleG (Located (ImpName Name)) -> Map Name ModParamNames
    forall mname. ModuleG mname -> Map Name ModParamNames
    mSignatures BIWhat
    BIInterface

        mkBad :: (ModuleG (Located (ImpName Name)) -> Map b a) -> a -> [(a, b)]
    mkBad ModuleG (Located (ImpName Name)) -> Map b a
    sel a
    a = [ (a
    a,b
    k) | b
    k <- Map b a -> [b]
    forall k a. Map k a -> [k]
    Map.keys (ModuleG (Located (ImpName Name)) -> Map b a
    sel ModuleG (Located (ImpName Name))
    m) ]

        ourPath :: ModPath
    ourPath = case Located (ImpName Name) -> ImpName Name
    forall a. Located a -> a
    thing (ModuleG (Located (ImpName Name)) -> Located (ImpName Name)
    forall mname. ModuleG mname -> mname
    mName ModuleG (Located (ImpName Name))
    m) of
                    ImpTop ModName
    mo    -> ModName -> ModPath
    TopModule ModName
    mo
                    ImpNested Name
    mo -> ModPath -> Ident -> ModPath
    Nested (Name -> ModPath
    nameModPath Name
    mo) (Name -> Ident
    nameIdent Name
    mo)

        doAddParams :: Map Name Newtype
    -> (ModuleG (Located (ImpName Name)) -> a) -> ReaderT RO InferM a
    doAddParams Map Name Newtype
    nt ModuleG (Located (ImpName Name)) -> a
    sel =
          (RO -> RO) -> ReaderT RO InferM a -> ReaderT RO InferM a
    forall (m :: * -> *) r a. RunReaderM m r => (r -> r) -> m a -> m a
    mapReader (\RO
    ro -> RO
    ro { newNewtypes :: Map Name Newtype
    newNewtypes = Map Name Newtype
    nt }) (a -> ReaderT RO InferM a
    forall t. AddParams t => t -> RewM t
    addParams (ModuleG (Located (ImpName Name)) -> a
    sel ModuleG (Located (ImpName Name))
    m))

    type RewM = ReaderT RO TC.InferM

    recordError :: Error -> RewM ()
    recordError :: Error -> ReaderT RO InferM ()
    recordError Error
    e = InferM () -> ReaderT RO InferM ()
    forall (m :: * -> *) a. Monad m => m a -> ReaderT RO m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (Error -> InferM ()
    TC.recordError Error
    e)

    data RO = RO
      { RO -> Name -> Bool
    isOurs       :: Name -> Bool
      , RO -> [MBQual TParam]
    tparams      :: [MBQual TParam]
      , RO -> [Prop]
    constraints  :: [Prop]
      , RO -> Map (MBQual Name) Prop
    vparams      :: Map (MBQual Name) Type
      , RO -> Map Name Newtype
    newNewtypes  :: Map Name Newtype
      }

    class AddParams t where
      addParams :: t -> RewM t

    instance AddParams a => AddParams (Map Name a) where
      addParams :: Map Name a -> RewM (Map Name a)
    addParams = (a -> ReaderT RO InferM a) -> Map Name a -> RewM (Map Name a)
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Map Name a -> m (Map Name b)
    mapM a -> ReaderT RO InferM a
    forall t. AddParams t => t -> RewM t
    addParams

    instance AddParams a => AddParams [a] where
      addParams :: [a] -> RewM [a]
    addParams = (a -> ReaderT RO InferM a) -> [a] -> RewM [a]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM a -> ReaderT RO InferM a
    forall t. AddParams t => t -> RewM t
    addParams

    instance AddParams Newtype where
      addParams :: Newtype -> RewM Newtype
    addParams Newtype
    nt =
        do (TypeParams
    tps,[Prop]
    cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
    newTypeParams Name -> TPFlavor
    TPNewtypeParam
           [Prop]
    rProps   <- TypeParams -> [Prop] -> RewM [Prop]
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    tps (Newtype -> [Prop]
    ntConstraints Newtype
    nt)
           RecordMap Ident Prop
    rFields  <- TypeParams -> RecordMap Ident Prop -> RewM (RecordMap Ident Prop)
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    tps (Newtype -> RecordMap Ident Prop
    ntFields Newtype
    nt)
           Newtype -> RewM Newtype
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Newtype
    nt
             { ntParams :: [TParam]
    ntParams       = TypeParams -> [TParam]
    forall decl use. Params decl use -> [decl]
    pDecl TypeParams
    tps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ Newtype -> [TParam]
    ntParams Newtype
    nt
             , ntConstraints :: [Prop]
    ntConstraints  = [Prop]
    cs [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    rProps
             , ntFields :: RecordMap Ident Prop
    ntFields       = RecordMap Ident Prop
    rFields
             }

    instance AddParams TySyn where
      addParams :: TySyn -> RewM TySyn
    addParams TySyn
    ts =
        do (TypeParams
    tps,[Prop]
    cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
    newTypeParams Name -> TPFlavor
    TPTySynParam
           [Prop]
    rProps   <- TypeParams -> [Prop] -> RewM [Prop]
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    tps (TySyn -> [Prop]
    tsConstraints TySyn
    ts)
           Prop
    rDef     <- TypeParams -> Prop -> RewM Prop
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    tps (TySyn -> Prop
    tsDef TySyn
    ts)
           TySyn -> RewM TySyn
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure TySyn
    ts
             { tsParams :: [TParam]
    tsParams      = TypeParams -> [TParam]
    forall decl use. Params decl use -> [decl]
    pDecl TypeParams
    tps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ TySyn -> [TParam]
    tsParams TySyn
    ts
             , tsConstraints :: [Prop]
    tsConstraints = [Prop]
    cs [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    rProps
             , tsDef :: Prop
    tsDef         = Prop
    rDef
             }

    instance AddParams DeclGroup where
      addParams :: DeclGroup -> RewM DeclGroup
    addParams DeclGroup
    dg =
        case DeclGroup
    dg of
          Recursive [Decl]
    ds   -> [Decl] -> DeclGroup
    Recursive ([Decl] -> DeclGroup) -> ReaderT RO InferM [Decl] -> RewM DeclGroup
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Decl] -> ReaderT RO InferM [Decl]
    forall t. AddParams t => t -> RewM t
    addParams [Decl]
    ds
          NonRecursive Decl
    d -> Decl -> DeclGroup
    NonRecursive (Decl -> DeclGroup) -> ReaderT RO InferM Decl -> RewM DeclGroup
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Decl -> ReaderT RO InferM Decl
    forall t. AddParams t => t -> RewM t
    addParams Decl
    d

    instance AddParams Decl where
      addParams :: Decl -> ReaderT RO InferM Decl
    addParams Decl
    d =
        case Decl -> DeclDef
    dDefinition Decl
    d of
          DeclDef
    DPrim       -> BIWhat -> ReaderT RO InferM Decl
    bad BIWhat
    BIPrimitive
          DForeign {} -> BIWhat -> ReaderT RO InferM Decl
    bad BIWhat
    BIForeign
          DExpr Expr
    e ->
            do (TypeParams
    tps,[Prop]
    cs) <- (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
    newTypeParams Name -> TPFlavor
    TPSchemaParam
               (ValParams
    vps,[(Name, Prop)]
    bs) <- TypeParams -> RewM (ValParams, [(Name, Prop)])
    newValParams TypeParams
    tps
               let s :: Schema
    s = Decl -> Schema
    dSignature Decl
    d

               Prop
    ty1 <- TypeParams -> Prop -> RewM Prop
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    tps (Schema -> Prop
    sType Schema
    s)
               [Prop]
    ps1 <- TypeParams -> [Prop] -> RewM [Prop]
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    tps (Schema -> [Prop]
    sProps Schema
    s)
               let ty2 :: Prop
    ty2 = (Prop -> Prop -> Prop) -> Prop -> [Prop] -> Prop
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Prop -> Prop -> Prop
    tFun Prop
    ty1 (((Name, Prop) -> Prop) -> [(Name, Prop)] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, Prop) -> Prop
    forall a b. (a, b) -> b
    snd [(Name, Prop)]
    bs)

               Expr
    e1 <- TypeParams -> Int -> ValParams -> Expr -> RewM Expr
    forall t. RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
    rewValM TypeParams
    tps ([Prop] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Prop]
    cs) ValParams
    vps Expr
    e
               let ([TParam]
    das,Expr
    e2) = (Expr -> Maybe (TParam, Expr)) -> Expr -> ([TParam], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (TParam, Expr)
    splitTAbs     Expr
    e1
                   ([Prop]
    dcs,Expr
    e3) = (Expr -> Maybe (Prop, Expr)) -> Expr -> ([Prop], Expr)
    forall a b. (a -> Maybe (b, a)) -> a -> ([b], a)
    splitWhile Expr -> Maybe (Prop, Expr)
    splitProofAbs Expr
    e2
                   e4 :: Expr
    e4 = ((Name, Prop) -> Expr -> Expr) -> Expr -> [(Name, Prop)] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Name -> Prop -> Expr -> Expr) -> (Name, Prop) -> Expr -> Expr
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Name -> Prop -> Expr -> Expr
    EAbs) Expr
    e3 [(Name, Prop)]
    bs
                   e5 :: Expr
    e5 = (Prop -> Expr -> Expr) -> Expr -> [Prop] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Prop -> Expr -> Expr
    EProofAbs Expr
    e4 ([Prop]
    cs [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    dcs)
                   e6 :: Expr
    e6 = (TParam -> Expr -> Expr) -> Expr -> [TParam] -> Expr
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr TParam -> Expr -> Expr
    ETAbs     Expr
    e5 (TypeParams -> [TParam]
    forall decl use. Params decl use -> [decl]
    pDecl TypeParams
    tps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ [TParam]
    das)

                   s1 :: Schema
    s1 = Forall
                          { sVars :: [TParam]
    sVars  = TypeParams -> [TParam]
    forall decl use. Params decl use -> [decl]
    pDecl TypeParams
    tps [TParam] -> [TParam] -> [TParam]
    forall a. [a] -> [a] -> [a]
    ++ Schema -> [TParam]
    sVars Schema
    s
                          , sProps :: [Prop]
    sProps = [Prop]
    cs [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop]
    ps1
                          , sType :: Prop
    sType  = Prop
    ty2
                          }

               Decl -> ReaderT RO InferM Decl
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Decl
    d { dDefinition :: DeclDef
    dDefinition = Expr -> DeclDef
    DExpr Expr
    e6
                      , dSignature :: Schema
    dSignature  = Schema
    s1
                      }
        where
        bad :: BIWhat -> ReaderT RO InferM Decl
    bad BIWhat
    w =
          do Error -> ReaderT RO InferM ()
    recordError (BadBacktickInstance -> Error
    FunctorInstanceBadBacktick ([(BIWhat, Name)] -> BadBacktickInstance
    BINested [(BIWhat
    w,Decl -> Name
    dName Decl
    d)]))
             Decl -> ReaderT RO InferM Decl
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Decl
    d

    data Params decl use = Params
      { forall decl use. Params decl use -> [decl]
    pDecl   :: [decl]
      , forall decl use. Params decl use -> [use]
    pUse    :: [use]
      , forall decl use. Params decl use -> Map decl use
    pSubst  :: Map decl use
      }

    noParams :: Params decl use
    noParams :: forall decl use. Params decl use
    noParams = Params
      { pDecl :: [decl]
    pDecl   = []
      , pUse :: [use]
    pUse    = []
      , pSubst :: Map decl use
    pSubst  = Map decl use
    forall k a. Map k a
    Map.empty
      }

    qualLabel :: Maybe ModName -> Ident -> Ident
    qualLabel :: Maybe ModName -> Ident -> Ident
    qualLabel Maybe ModName
    mb Ident
    i =
      case Maybe ModName
    mb of
        Maybe ModName
    Nothing -> Ident
    i
        Just ModName
    mn ->
          let txt :: Text
    txt = Text -> [Text] -> Text
    Text.intercalate Text
    "'" (ModName -> [Text]
    modNameChunksText ModName
    mn [Text] -> [Text] -> [Text]
    forall a. [a] -> [a] -> [a]
    ++ [Ident -> Text
    identText Ident
    i])
          in Text -> Ident
    mkIdent Text
    txt

    type TypeParams = Params TParam Type
    type ValParams  = Params Name   Expr

    newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams,[Prop])
    newTypeParams :: (Name -> TPFlavor) -> RewM (TypeParams, [Prop])
    newTypeParams Name -> TPFlavor
    flav =
      do RO
    ro <- ReaderT RO InferM RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         let newFlaf :: Maybe ModName -> Name -> TPFlavor
    newFlaf Maybe ModName
    q = Name -> TPFlavor
    flav (Name -> TPFlavor) -> (Name -> Name) -> Name -> TPFlavor
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Ident -> Ident) -> Name -> Name
    mapNameIdent (Maybe ModName -> Ident -> Ident
    qualLabel Maybe ModName
    q)
         [TParam]
    as <- InferM [TParam] -> ReaderT RO InferM [TParam]
    forall (m :: * -> *) a. Monad m => m a -> ReaderT RO m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift ([MBQual TParam]
    -> (MBQual TParam -> InferM TParam) -> InferM [TParam]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (RO -> [MBQual TParam]
    tparams RO
    ro) \(Maybe ModName
    q,TParam
    a) -> (Name -> TPFlavor) -> TParam -> InferM TParam
    TC.freshTParam (Maybe ModName -> Name -> TPFlavor
    newFlaf Maybe ModName
    q) TParam
    a)
         let bad :: [Ident]
    bad = [ Ident
    x
                   | Ident
    x : Ident
    _ : [Ident]
    _ <- [Ident] -> [[Ident]]
    forall a. Eq a => [a] -> [[a]]
    group ([Ident] -> [Ident]
    forall a. Ord a => [a] -> [a]
    sort ((Name -> Ident) -> [Name] -> [Ident]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Ident
    nameIdent ((TParam -> Maybe Name) -> [TParam] -> [Name]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe TParam -> Maybe Name
    tpName [TParam]
    as)))
                   ]
         [Ident] -> (Ident -> ReaderT RO InferM ()) -> ReaderT RO InferM ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ [Ident]
    bad \Ident
    i ->
           Error -> ReaderT RO InferM ()
    recordError (BadBacktickInstance -> Error
    FunctorInstanceBadBacktick (Ident -> BadBacktickInstance
    BIMultipleParams Ident
    i))

         let ts :: [Prop]
    ts = (TParam -> Prop) -> [TParam] -> [Prop]
    forall a b. (a -> b) -> [a] -> [b]
    map (TVar -> Prop
    TVar (TVar -> Prop) -> (TParam -> TVar) -> TParam -> Prop
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TParam -> TVar
    TVBound) [TParam]
    as
             su :: Map TParam Prop
    su = [(TParam, Prop)] -> Map TParam Prop
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList ([TParam] -> [Prop] -> [(TParam, Prop)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip ((MBQual TParam -> TParam) -> [MBQual TParam] -> [TParam]
    forall a b. (a -> b) -> [a] -> [b]
    map MBQual TParam -> TParam
    forall a b. (a, b) -> b
    snd (RO -> [MBQual TParam]
    tparams RO
    ro)) [Prop]
    ts)
             ps :: TypeParams
    ps = Params { pDecl :: [TParam]
    pDecl = [TParam]
    as, pUse :: [Prop]
    pUse = [Prop]
    ts, pSubst :: Map TParam Prop
    pSubst = Map TParam Prop
    su }
         [Prop]
    cs <- TypeParams -> [Prop] -> RewM [Prop]
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    ps (RO -> [Prop]
    constraints RO
    ro)
         (TypeParams, [Prop]) -> RewM (TypeParams, [Prop])
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TypeParams
    ps,[Prop]
    cs)

    -- Note: we pass all value parameters as a record
    newValParams :: TypeParams -> RewM (ValParams, [(Name,Type)])
    newValParams :: TypeParams -> RewM (ValParams, [(Name, Prop)])
    newValParams TypeParams
    tps =
      do RO
    ro <- ReaderT RO InferM RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         let vps :: Map (MBQual Name) Prop
    vps = RO -> Map (MBQual Name) Prop
    vparams RO
    ro
         if Map (MBQual Name) Prop -> Bool
    forall k a. Map k a -> Bool
    Map.null Map (MBQual Name) Prop
    vps
           then (ValParams, [(Name, Prop)]) -> RewM (ValParams, [(Name, Prop)])
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ValParams
    forall decl use. Params decl use
    noParams, [])
           else do [(Name, Ident, Prop)]
    xts <- [(MBQual Name, Prop)]
    -> ((MBQual Name, Prop) -> ReaderT RO InferM (Name, Ident, Prop))
    -> ReaderT RO InferM [(Name, Ident, Prop)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM (Map (MBQual Name) Prop -> [(MBQual Name, Prop)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map (MBQual Name) Prop
    vps) \((Maybe ModName
    q,Name
    x),Prop
    t) ->
                            do Prop
    t1 <- TypeParams -> Prop -> RewM Prop
    forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    tps Prop
    t
                               let l :: Ident
    l = Maybe ModName -> Ident -> Ident
    qualLabel Maybe ModName
    q (Name -> Ident
    nameIdent Name
    x)
                               (Name, Ident, Prop) -> ReaderT RO InferM (Name, Ident, Prop)
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Name
    x, Ident
    l, Prop
    t1)
                   let ([Name]
    xs,[Ident]
    ls,[Prop]
    ts) = [(Name, Ident, Prop)] -> ([Name], [Ident], [Prop])
    forall a b c. [(a, b, c)] -> ([a], [b], [c])
    unzip3 [(Name, Ident, Prop)]
    xts
                       fs :: [(Ident, Prop)]
    fs      = [Ident] -> [Prop] -> [(Ident, Prop)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Ident]
    ls [Prop]
    ts
                       sel :: Ident -> Selector
    sel Ident
    l   = Ident -> Maybe [Ident] -> Selector
    RecordSel Ident
    l ([Ident] -> Maybe [Ident]
    forall a. a -> Maybe a
    Just [Ident]
    ls)

                   Prop
    t <- case [(Ident, Prop)] -> Either (Ident, Prop) (RecordMap Ident Prop)
    forall a b.
    (Show a, Ord a) =>
    [(a, b)] -> Either (a, b) (RecordMap a b)
    recordFromFieldsErr [(Ident, Prop)]
    fs of
                          Right RecordMap Ident Prop
    ok -> Prop -> RewM Prop
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (RecordMap Ident Prop -> Prop
    TRec RecordMap Ident Prop
    ok)
                          Left (Ident
    x,Prop
    _) ->
                            do Error -> ReaderT RO InferM ()
    recordError (BadBacktickInstance -> Error
    FunctorInstanceBadBacktick
                                              (Ident -> BadBacktickInstance
    BIMultipleParams Ident
    x))
                               Prop -> RewM Prop
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (RecordMap Ident Prop -> Prop
    TRec ([(Ident, Prop)] -> RecordMap Ident Prop
    forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
    recordFromFields [(Ident, Prop)]
    fs))

                   Name
    r <- InferM Name -> ReaderT RO InferM Name
    forall (m :: * -> *) a. Monad m => m a -> ReaderT RO m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadT t, Monad m) =>
    m a -> t m a
    lift (Namespace -> Ident -> InferM Name
    TC.newLocalName Namespace
    NSValue (Text -> Ident
    mkIdent Text
    "params"))
                   let e :: Expr
    e = Name -> Expr
    EVar Name
    r
                   (ValParams, [(Name, Prop)]) -> RewM (ValParams, [(Name, Prop)])
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
                     ( Params
                         { pDecl :: [Name]
    pDecl  = [Name
    r]
                         , pUse :: [Expr]
    pUse   = [Expr
    e]
                         , pSubst :: Map Name Expr
    pSubst = [(Name, Expr)] -> Map Name Expr
    forall k a. Ord k => [(k, a)] -> Map k a
    Map.fromList [ (Name
    x,Expr -> Selector -> Expr
    ESel Expr
    e (Ident -> Selector
    sel Ident
    l))
                                                 | (Name
    x,Ident
    l) <- [Name] -> [Ident] -> [(Name, Ident)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Name]
    xs [Ident]
    ls ]
                         }
                     , [ (Name
    r,Prop
    t) ]
                     )

    liftRew ::
      ((?isOurs :: Name -> Bool, ?newNewtypes :: Map Name Newtype) => a) ->
      RewM a
    liftRew :: forall a.
    ((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
    -> RewM a
    liftRew (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a
    x =
      do RO
    ro <- ReaderT RO InferM RO
    forall (m :: * -> *) i. ReaderM m i => m i
    ask
         let ?isOurs      = RO -> Name -> Bool
    isOurs RO
    ro
             ?newNewtypes = RO -> Map Name Newtype
    newNewtypes RO
    ro
         a -> RewM a
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a
    x

    rewTypeM :: RewType t => TypeParams -> t -> RewM t
    rewTypeM :: forall t. RewType t => TypeParams -> t -> RewM t
    rewTypeM TypeParams
    ps t
    x =
      do let ?tparams = ?tparams::TypeParams
    TypeParams
    ps
         ((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t)
    -> RewM (t -> t)
    forall a.
    ((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
    -> RewM a
    liftRew t -> t
    (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType RewM (t -> t) -> RewM t -> RewM t
    forall a b.
    ReaderT RO InferM (a -> b)
    -> ReaderT RO InferM a -> ReaderT RO InferM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> t -> RewM t
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure t
    x

    rewValM :: RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
    rewValM :: forall t. RewVal t => TypeParams -> Int -> ValParams -> t -> RewM t
    rewValM TypeParams
    ts Int
    cs ValParams
    vs t
    x =
      do let ?tparams = ?tparams::TypeParams
    TypeParams
    ts
             ?cparams = ?cparams::Int
    Int
    cs
             ?vparams = ?vparams::ValParams
    ValParams
    vs
         ((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t)
    -> RewM (t -> t)
    forall a.
    ((?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => a)
    -> RewM a
    liftRew t -> t
    (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype) => t -> t
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew RewM (t -> t) -> RewM t -> RewM t
    forall a b.
    ReaderT RO InferM (a -> b)
    -> ReaderT RO InferM a -> ReaderT RO InferM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> t -> RewM t
    forall a. a -> ReaderT RO InferM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure t
    x

    class RewType t where
      rewType ::
        ( ?isOurs      :: Name -> Bool
        , ?newNewtypes :: Map Name Newtype    -- Lazy
        , ?tparams     :: TypeParams
        ) => t -> t

    instance RewType Type where
      rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    Prop -> Prop
    rewType Prop
    ty =
        case Prop
    ty of

          TCon TCon
    tc [Prop]
    ts
            | TC (TCAbstract (UserTC Name
    x Kind
    _)) <- TCon
    tc
            , ?isOurs::Name -> Bool
    Name -> Bool
    ?isOurs Name
    x  -> TCon -> [Prop] -> Prop
    TCon TCon
    tc (TypeParams -> [Prop]
    forall decl use. Params decl use -> [use]
    pUse ?tparams::TypeParams
    TypeParams
    ?tparams [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType [Prop]
    ts)
            | Bool
    otherwise  -> TCon -> [Prop] -> Prop
    TCon TCon
    tc ([Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType [Prop]
    ts)

          TVar TVar
    x ->
            case TVar
    x of
              TVBound TParam
    x' ->
                case TParam -> Map TParam Prop -> Maybe Prop
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup TParam
    x' (TypeParams -> Map TParam Prop
    forall decl use. Params decl use -> Map decl use
    pSubst ?tparams::TypeParams
    TypeParams
    ?tparams) of
                  Just Prop
    t  -> Prop
    t
                  Maybe Prop
    Nothing -> Prop
    ty
              TVFree {} -> String -> [String] -> Prop
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "rawType" [String
    "Free unification variable"]

          TUser Name
    f [Prop]
    ts Prop
    t
            | ?isOurs::Name -> Bool
    Name -> Bool
    ?isOurs Name
    f -> Name -> [Prop] -> Prop -> Prop
    TUser Name
    f (TypeParams -> [Prop]
    forall decl use. Params decl use -> [use]
    pUse ?tparams::TypeParams
    TypeParams
    ?tparams [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType [Prop]
    ts) (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t)
            | Bool
    otherwise -> Name -> [Prop] -> Prop -> Prop
    TUser Name
    f ([Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType [Prop]
    ts) (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t)

          TRec RecordMap Ident Prop
    fs -> RecordMap Ident Prop -> Prop
    TRec (RecordMap Ident Prop -> RecordMap Ident Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType RecordMap Ident Prop
    fs)

          TNewtype Newtype
    tdef [Prop]
    ts
            | ?isOurs::Name -> Bool
    Name -> Bool
    ?isOurs Name
    nm -> Newtype -> [Prop] -> Prop
    TNewtype Newtype
    tdef' (TypeParams -> [Prop]
    forall decl use. Params decl use -> [use]
    pUse ?tparams::TypeParams
    TypeParams
    ?tparams [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType [Prop]
    ts)
            | Bool
    otherwise  -> Newtype -> [Prop] -> Prop
    TNewtype Newtype
    tdef ([Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType [Prop]
    ts)
            where
            nm :: Name
    nm    = Newtype -> Name
    ntName Newtype
    tdef
            tdef' :: Newtype
    tdef' = case Name -> Map Name Newtype -> Maybe Newtype
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    nm ?newNewtypes::Map Name Newtype
    Map Name Newtype
    ?newNewtypes of
                      Just Newtype
    yes -> Newtype
    yes
                      Maybe Newtype
    Nothing  -> String -> [String] -> Newtype
    forall a. HasCallStack => String -> [String] -> a
    panic String
    "rewType" [ String
    "Missing recursive newtype"
                                                  , Doc -> String
    forall a. Show a => a -> String
    show (Name -> Doc
    forall a. PP a => a -> Doc
    pp Name
    nm) ]

    instance RewType a => RewType [a] where
      rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    [a] -> [a]
    rewType = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> a
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType

    instance RewType b => RewType (RecordMap a b) where
      rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    RecordMap a b -> RecordMap a b
    rewType = (b -> b) -> RecordMap a b -> RecordMap a b
    forall a b. (a -> b) -> RecordMap a a -> RecordMap a b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b -> b
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType

    instance RewType Schema where
      rewType :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    Schema -> Schema
    rewType Schema
    sch =
        Forall { sVars :: [TParam]
    sVars  = Schema -> [TParam]
    sVars Schema
    sch
               , sProps :: [Prop]
    sProps = [Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType (Schema -> [Prop]
    sProps Schema
    sch)
               , sType :: Prop
    sType  = Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType (Schema -> Prop
    sType Schema
    sch)
               }

    class RewVal t where
      rew ::
        ( ?isOurs      :: Name -> Bool
        , ?newNewtypes :: Map Name Newtype    -- Lazy
        , ?tparams     :: TypeParams
        , ?cparams     :: Int                 -- Number of constraitns
        , ?vparams     :: ValParams
        ) => t -> t

    instance RewVal a => RewVal [a] where
      rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    [a] -> [a]
    rew = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> a
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew

    instance RewVal b => RewVal (RecordMap a b) where
      rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    RecordMap a b -> RecordMap a b
    rew = (b -> b) -> RecordMap a b -> RecordMap a b
    forall a b. (a -> b) -> RecordMap a a -> RecordMap a b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap b -> b
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew

    {- x as cs vs  -->
       e (newAs ++ as) (newCS ++ cs) (newVS ++ vs)
    -}
    instance RewVal Expr where
      rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    Expr -> Expr
    rew Expr
    expr =
        case Expr
    expr of
          EList [Expr]
    es Prop
    t        -> [Expr] -> Prop -> Expr
    EList ([Expr] -> [Expr]
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew [Expr]
    es) (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t)
          ETuple [Expr]
    es         -> [Expr] -> Expr
    ETuple ([Expr] -> [Expr]
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew [Expr]
    es)
          ERec RecordMap Ident Expr
    fs           -> RecordMap Ident Expr -> Expr
    ERec (RecordMap Ident Expr -> RecordMap Ident Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew RecordMap Ident Expr
    fs)
          ESel Expr
    e Selector
    l          -> Expr -> Selector -> Expr
    ESel (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e) Selector
    l
          ESet Prop
    t Expr
    e1 Selector
    s Expr
    e2    -> Prop -> Expr -> Selector -> Expr -> Expr
    ESet (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e1) Selector
    s (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e2)
          EIf Expr
    e1 Expr
    e2 Expr
    e3      -> Expr -> Expr -> Expr -> Expr
    EIf (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e1) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e2) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e3)
          EComp Prop
    t1 Prop
    t2 Expr
    e [[Match]]
    mss -> Prop -> Prop -> Expr -> [[Match]] -> Expr
    EComp (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t1) (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t2) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e) ([[Match]] -> [[Match]]
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew [[Match]]
    mss)
          EVar Name
    x            -> Expr -> Expr
    forall {decl}.
    (?tparams::TypeParams, ?isOurs::Name -> Bool,
     ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
     ?cparams::Int) =>
    Expr -> Expr
    tryVarApp
                               case Name -> Map Name Expr -> Maybe Expr
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Name
    x (ValParams -> Map Name Expr
    forall decl use. Params decl use -> Map decl use
    pSubst ?vparams::ValParams
    ValParams
    ?vparams) of
                                 Just Expr
    p  -> Expr
    p
                                 Maybe Expr
    Nothing -> Expr
    expr

          ETApp Expr
    e Prop
    t         -> Expr -> Expr
    forall {decl}.
    (?tparams::TypeParams, ?isOurs::Name -> Bool,
     ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
     ?cparams::Int) =>
    Expr -> Expr
    tryVarApp (Expr -> Prop -> Expr
    ETApp (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e) (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t))
          EProofApp Expr
    e       -> Expr -> Expr
    forall {decl}.
    (?tparams::TypeParams, ?isOurs::Name -> Bool,
     ?vparams::Params decl Expr, ?newNewtypes::Map Name Newtype,
     ?cparams::Int) =>
    Expr -> Expr
    tryVarApp (Expr -> Expr
    EProofApp (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e))

          EApp Expr
    e1 Expr
    e2        -> Expr -> Expr -> Expr
    EApp (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e1) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e2)
          ETAbs TParam
    a Expr
    e         -> TParam -> Expr -> Expr
    ETAbs TParam
    a (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e)
          EAbs Name
    x Prop
    t Expr
    e        -> Name -> Prop -> Expr -> Expr
    EAbs Name
    x (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e)
          ELocated Range
    r Expr
    e      -> Range -> Expr -> Expr
    ELocated Range
    r (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e)
          EProofAbs Prop
    p Expr
    e     -> Prop -> Expr -> Expr
    EProofAbs (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    p) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e)
          EWhere Expr
    e [DeclGroup]
    ds       -> Expr -> [DeclGroup] -> Expr
    EWhere (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e) ([DeclGroup] -> [DeclGroup]
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew [DeclGroup]
    ds)
          EPropGuards [([Prop], Expr)]
    gs Prop
    t  -> [([Prop], Expr)] -> Prop -> Expr
    EPropGuards [([Prop], Expr)]
    gs' (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t)
            where gs' :: [([Prop], Expr)]
    gs' = [ (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType (Prop -> Prop) -> [Prop] -> [Prop]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Prop]
    p, Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e) | ([Prop]
    p,Expr
    e) <- [([Prop], Expr)]
    gs ]

        where
        tryVarApp :: Expr -> Expr
    tryVarApp Expr
    orElse =
          case Expr -> (Expr, [Prop], Int)
    splitExprInst Expr
    expr of
            (EVar Name
    x, [Prop]
    ts, Int
    cs) | ?isOurs::Name -> Bool
    Name -> Bool
    ?isOurs Name
    x ->
               let ets :: Expr
    ets = (Expr -> Prop -> Expr) -> Expr -> [Prop] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Expr -> Prop -> Expr
    ETApp (Name -> Expr
    EVar Name
    x) (TypeParams -> [Prop]
    forall decl use. Params decl use -> [use]
    pUse ?tparams::TypeParams
    TypeParams
    ?tparams [Prop] -> [Prop] -> [Prop]
    forall a. [a] -> [a] -> [a]
    ++ [Prop] -> [Prop]
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType [Prop]
    ts)
                   eps :: Expr
    eps = (Expr -> Expr) -> Expr -> [Expr]
    forall a. (a -> a) -> a -> [a]
    iterate Expr -> Expr
    EProofApp Expr
    ets [Expr] -> Int -> Expr
    forall a. HasCallStack => [a] -> Int -> a
    !! (?cparams::Int
    Int
    ?cparams Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    cs)
                   evs :: Expr
    evs = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Expr -> Expr -> Expr
    EApp Expr
    eps (Params decl Expr -> [Expr]
    forall decl use. Params decl use -> [use]
    pUse ?vparams::Params decl Expr
    Params decl Expr
    ?vparams)
               in Expr
    evs
            (Expr, [Prop], Int)
    _ -> Expr
    orElse

    instance RewVal DeclGroup where
      rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    DeclGroup -> DeclGroup
    rew DeclGroup
    dg =
        case DeclGroup
    dg of
          Recursive [Decl]
    ds    -> [Decl] -> DeclGroup
    Recursive ([Decl] -> [Decl]
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew [Decl]
    ds)
          NonRecursive Decl
    d  -> Decl -> DeclGroup
    NonRecursive (Decl -> Decl
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Decl
    d)

    instance RewVal Decl where
      rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    Decl -> Decl
    rew Decl
    d = Decl
    d { dDefinition :: DeclDef
    dDefinition = DeclDef -> DeclDef
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew (Decl -> DeclDef
    dDefinition Decl
    d)
                , dSignature :: Schema
    dSignature  = Schema -> Schema
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType (Decl -> Schema
    dSignature Decl
    d)
                }

    instance RewVal DeclDef where
      rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    DeclDef -> DeclDef
    rew DeclDef
    def =
        case DeclDef
    def of
          DeclDef
    DPrim       -> DeclDef
    def
          DForeign {} -> DeclDef
    def
          DExpr Expr
    e     -> Expr -> DeclDef
    DExpr (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e)

    instance RewVal Match where
      rew :: (?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    Match -> Match
    rew Match
    ma =
        case Match
    ma of
          From Name
    x Prop
    t1 Prop
    t2 Expr
    e -> Name -> Prop -> Prop -> Expr -> Match
    From Name
    x (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t1) (Prop -> Prop
    forall t.
    (RewType t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams) =>
    t -> t
    rewType Prop
    t2) (Expr -> Expr
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Expr
    e)
          Let Decl
    d          -> Decl -> Match
    Let (Decl -> Decl
    forall t.
    (RewVal t, ?isOurs::Name -> Bool, ?newNewtypes::Map Name Newtype,
     ?tparams::TypeParams, ?cparams::Int, ?vparams::ValParams) =>
    t -> t
    rew Decl
    d)