    -- | Translating Agda types to Haskell types. Used to ensure that imported
    --   Haskell functions have the right type.

    module Agda.Compiler.MAlonzo.HaskellTypes
      ( haskellType
      , hsTelApproximation, hsTelApproximation'
      ) where

    import Control.Monad         ( zipWithM )
    import Control.Monad.Except  ( ExceptT(ExceptT), runExceptT, mapExceptT, catchError, throwError )
    import Control.Monad.Trans   ( lift )

    import Data.Maybe (fromMaybe)
    import Data.List (intercalate)

    import Agda.Syntax.Position
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Telescope

    import Agda.Compiler.MAlonzo.Pragmas
    import Agda.Compiler.MAlonzo.Misc
    import Agda.Compiler.MAlonzo.Pretty () --instance only

    import qualified Agda.Utils.Haskell.Syntax as HS
    import Agda.Utils.List
    import Agda.Utils.Monad
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty (prettyShow)

    import Agda.Utils.Impossible

    hsQCon :: String -> String -> HS.Type
    hsQCon :: String -> String -> Type
    hsQCon String
    m String
    f = QName -> Type
    HS.TyCon (QName -> Type) -> QName -> Type
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> Name -> QName
    HS.Qual (String -> ModuleName
    HS.ModuleName String
    m) (String -> Name
    HS.Ident String
    f)

    hsCon :: String -> HS.Type
    hsCon :: String -> Type
    hsCon = QName -> Type
    HS.TyCon (QName -> Type) -> (String -> QName) -> String -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> QName
    HS.UnQual (Name -> QName) -> (String -> Name) -> String -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Name
    HS.Ident

    hsUnit :: HS.Type
    hsUnit :: Type
    hsUnit = String -> Type
    hsCon String
    "()"

    hsVar :: HS.Name -> HS.Type
    hsVar :: Name -> Type
    hsVar = Name -> Type
    HS.TyVar

    hsApp :: HS.Type -> [HS.Type] -> HS.Type
    hsApp :: Type -> [Type] -> Type
    hsApp Type
    d [Type]
    ds = (Type -> Type -> Type) -> Type -> [Type] -> Type
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Type -> Type -> Type
    HS.TyApp Type
    d [Type]
    ds

    hsForall :: HS.Name -> HS.Type -> HS.Type
    hsForall :: Name -> Type -> Type
    hsForall Name
    x = [TyVarBind] -> Type -> Type
    HS.TyForall [Name -> TyVarBind
    HS.UnkindedVar Name
    x]

    -- Issue #5207: From ghc-9.0 we have to be careful with nested foralls.
    hsFun :: HS.Type -> HS.Type -> HS.Type
    hsFun :: Type -> Type -> Type
    hsFun Type
    a (HS.TyForall [TyVarBind]
    vs Type
    b) = [TyVarBind] -> Type -> Type
    HS.TyForall [TyVarBind]
    vs (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ Type -> Type -> Type
    hsFun Type
    a Type
    b
    hsFun Type
    a Type
    b = Type -> Type -> Type
    HS.TyFun Type
    a Type
    b

    type ToHs = ExceptT WhyNotAHaskellType HsCompileM

    runToHs :: Term -> ToHs a -> HsCompileM a
    runToHs :: forall a. Term -> ToHs a -> HsCompileM a
    runToHs Term
    top ToHs a
    m = (WhyNotAHaskellType
     -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
    -> (a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
    -> Either WhyNotAHaskellType a
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (GHCBackendError
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    GHCBackendError -> m a
    ghcBackendError (GHCBackendError
     -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
    -> (WhyNotAHaskellType -> GHCBackendError)
    -> WhyNotAHaskellType
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> WhyNotAHaskellType -> GHCBackendError
    NotAHaskellType Term
    top) a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Either WhyNotAHaskellType a
     -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
    -> ReaderT
         GHCModuleEnv
         (StateT HsCompileState (TCMT IO))
         (Either WhyNotAHaskellType a)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< ToHs a
    -> ReaderT
         GHCModuleEnv
         (StateT HsCompileState (TCMT IO))
         (Either WhyNotAHaskellType a)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT ToHs a
    m

    liftE1' :: (forall b. (a -> m b) -> m b) -> (a -> ExceptT e m b) -> ExceptT e m b
    liftE1' :: forall a (m :: * -> *) e b.
    (forall b. (a -> m b) -> m b)
    -> (a -> ExceptT e m b) -> ExceptT e m b
    liftE1' forall b. (a -> m b) -> m b
    f a -> ExceptT e m b
    k = m (Either e b) -> ExceptT e m b
    forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
    ExceptT ((a -> m (Either e b)) -> m (Either e b)
    forall b. (a -> m b) -> m b
    f (ExceptT e m b -> m (Either e b)
    forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
    runExceptT (ExceptT e m b -> m (Either e b))
    -> (a -> ExceptT e m b) -> a -> m (Either e b)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> ExceptT e m b
    k))

    -- Only used in hsTypeApproximation below, and in that case we catch the error.
    getHsType' :: QName -> HsCompileM HS.Type
    getHsType' :: QName -> HsCompileM Type
    getHsType' QName
    q = Term -> ToHs Type -> HsCompileM Type
    forall a. Term -> ToHs a -> HsCompileM a
    runToHs (QName -> Elims -> Term
    Def QName
    q []) (QName -> ToHs Type
    getHsType QName
    q)

    getHsType :: QName -> ToHs HS.Type
    getHsType :: QName -> ToHs Type
    getHsType QName
    x = do
      ExceptT WhyNotAHaskellType HsCompileM Bool
    -> ExceptT WhyNotAHaskellType HsCompileM ()
    -> ExceptT WhyNotAHaskellType HsCompileM ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    unlessM (QName -> ExceptT WhyNotAHaskellType HsCompileM Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isCompiled QName
    x) (ExceptT WhyNotAHaskellType HsCompileM ()
     -> ExceptT WhyNotAHaskellType HsCompileM ())
    -> ExceptT WhyNotAHaskellType HsCompileM ()
    -> ExceptT WhyNotAHaskellType HsCompileM ()
    forall a b. (a -> b) -> a -> b
    $ WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM ()
    forall a.
    WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM ())
    -> WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM ()
    forall a b. (a -> b) -> a -> b
    $ QName -> WhyNotAHaskellType
    NotCompiled QName
    x

      d   <- TCM (Maybe HaskellPragma)
    -> ExceptT WhyNotAHaskellType HsCompileM (Maybe HaskellPragma)
    forall a. TCM a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM (Maybe HaskellPragma)
     -> ExceptT WhyNotAHaskellType HsCompileM (Maybe HaskellPragma))
    -> TCM (Maybe HaskellPragma)
    -> ExceptT WhyNotAHaskellType HsCompileM (Maybe HaskellPragma)
    forall a b. (a -> b) -> a -> b
    $ QName -> TCM (Maybe HaskellPragma)
    getHaskellPragma QName
    x
      env <- askGHCEnv
      let is QName
    t GHCEnv -> Maybe QName
    p = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    t Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    p GHCEnv
    env

          namedType = do
            -- For these builtin types, the type name (xhqn ...) refers to the
            -- generated, but unused, datatype and not the primitive type.
            if  | QName
    x QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvNat Bool -> Bool -> Bool
    ||
                  QName
    x QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvInteger -> Type -> ToHs Type
    forall a. a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> ToHs Type) -> Type -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    hsCon String
    "Integer"
                | QName
    x QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvBool    -> Type -> ToHs Type
    forall a. a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> ToHs Type) -> Type -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    hsCon String
    "Bool"
                | Bool
    otherwise            ->
                  HsCompileM Type -> ToHs Type
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ExceptT WhyNotAHaskellType m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (HsCompileM Type -> ToHs Type) -> HsCompileM Type -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    hsCon (String -> Type) -> (QName -> String) -> QName -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> String
    forall a. Pretty a => a -> String
    prettyShow (QName -> Type)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    -> HsCompileM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NameKind
    -> QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    xhqn NameKind
    TypeK QName
    x
      mapExceptT (setCurrentRange d) $ case d of
        Maybe HaskellPragma
    _ | QName
    x QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvList ->
            HsCompileM Type -> ToHs Type
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ExceptT WhyNotAHaskellType m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (HsCompileM Type -> ToHs Type) -> HsCompileM Type -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    hsCon (String -> Type) -> (QName -> String) -> QName -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> String
    forall a. Pretty a => a -> String
    prettyShow (QName -> Type)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    -> HsCompileM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NameKind
    -> QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    xhqn NameKind
    TypeK QName
    x
            -- we ignore Haskell pragmas for List
        Maybe HaskellPragma
    _ | QName
    x QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvMaybe ->
            HsCompileM Type -> ToHs Type
    forall (m :: * -> *) a.
    Monad m =>
    m a -> ExceptT WhyNotAHaskellType m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (HsCompileM Type -> ToHs Type) -> HsCompileM Type -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    hsCon (String -> Type) -> (QName -> String) -> QName -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> String
    forall a. Pretty a => a -> String
    prettyShow (QName -> Type)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    -> HsCompileM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NameKind
    -> QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    xhqn NameKind
    TypeK QName
    x
            -- we ignore Haskell pragmas for Maybe
        Maybe HaskellPragma
    _ | QName
    x QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvInf ->
            Type -> ToHs Type
    forall a. a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> ToHs Type) -> Type -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ String -> String -> Type
    hsQCon String
    "MAlonzo.RTE" String
    "Infinity"
        Just HsDefn{}      -> WhyNotAHaskellType -> ToHs Type
    forall a.
    WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (WhyNotAHaskellType -> ToHs Type)
    -> WhyNotAHaskellType -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ Range -> QName -> WhyNotAHaskellType
    WrongPragmaFor (Maybe HaskellPragma -> Range
    forall a. HasRange a => a -> Range
    getRange Maybe HaskellPragma
    d) QName
    x
        Just HsType{}      -> ToHs Type
    namedType
        Just HsData{}      -> ToHs Type
    namedType
        Maybe HaskellPragma
    _                  -> WhyNotAHaskellType -> ToHs Type
    forall a.
    WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (WhyNotAHaskellType -> ToHs Type)
    -> WhyNotAHaskellType -> ToHs Type
    forall a b. (a -> b) -> a -> b
    $ QName -> WhyNotAHaskellType
    NoPragmaFor QName
    x

    -- | Is the given thing compiled?

    isCompiled :: HasConstInfo m => QName -> m Bool
    isCompiled :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isCompiled QName
    q = Definition -> Bool
    forall a. LensModality a => a -> Bool
    usableModality (Definition -> Bool) -> m Definition -> m Bool
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q

    -- | Does the name stand for a data or record type?

    isData :: HasConstInfo m => QName -> m Bool
    isData :: forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isData QName
    q = do
      def <- Definition -> Defn
    theDef (Definition -> Defn) -> m Definition -> m Defn
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> m Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      return $ case def of
        Datatype{} -> Bool
    True
        Record{}   -> Bool
    True
        Defn
    _          -> Bool
    False

    getHsVar :: (MonadDebug tcm, MonadTCM tcm) => Nat -> tcm HS.Name
    getHsVar :: forall (tcm :: * -> *).
    (MonadDebug tcm, MonadTCM tcm) =>
    Int -> tcm Name
    getHsVar Int
    i =
      String -> Name
    HS.Ident (String -> Name) -> (Name -> String) -> Name -> Name
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NameKind -> String -> String
    encodeString (VariableKind -> NameKind
    VarK VariableKind
    X) (String -> String) -> (Name -> String) -> Name -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> String
    forall a. Pretty a => a -> String
    prettyShow (Name -> Name) -> tcm Name -> tcm Name
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> tcm Name
    forall (m :: * -> *). (MonadDebug m, MonadTCEnv m) => Int -> m Name
    nameOfBV Int
    i

    haskellType' :: Type -> HsCompileM HS.Type
    haskellType' :: Type -> HsCompileM Type
    haskellType' Type
    t = Term -> ToHs Type -> HsCompileM Type
    forall a. Term -> ToHs a -> HsCompileM a
    runToHs (Type -> Term
    forall t a. Type'' t a -> a
    unEl Type
    t) (Type -> ToHs Type
    fromType Type
    t)
      where
        fromArgs :: [Arg Term] -> ExceptT WhyNotAHaskellType HsCompileM [Type]
    fromArgs = (Arg Term -> ToHs Type)
    -> [Arg Term] -> ExceptT WhyNotAHaskellType HsCompileM [Type]
    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 (Term -> ToHs Type
    fromTerm (Term -> ToHs Type) -> (Arg Term -> Term) -> Arg Term -> ToHs Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg)
        fromType :: Type -> ToHs Type
    fromType = Term -> ToHs Type
    fromTerm (Term -> ToHs Type) -> (Type -> Term) -> Type -> ToHs Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Type -> Term
    forall t a. Type'' t a -> a
    unEl
        fromTerm :: Term -> ToHs Type
    fromTerm Term
    v = do
          v   <- TCM Term -> ExceptT WhyNotAHaskellType HsCompileM Term
    forall a. TCM a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (tcm :: * -> *) a. MonadTCM tcm => TCM a -> tcm a
    liftTCM (TCM Term -> ExceptT WhyNotAHaskellType HsCompileM Term)
    -> TCM Term -> ExceptT WhyNotAHaskellType HsCompileM Term
    forall a b. (a -> b) -> a -> b
    $ Term -> Term
    unSpine (Term -> Term) -> TCM Term -> TCM Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> TCM Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    v
          reportSDoc "compile.haskell.type" 25 $ "toHaskellType " <+> prettyTCM v
          reportSDoc "compile.haskell.type" 50 $ "toHaskellType " <+> pretty v
          kit <- liftTCM coinductionKit
          case v of
            Var Int
    x Elims
    es -> do
              let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
              Type -> [Type] -> Type
    hsApp (Type -> [Type] -> Type)
    -> (Name -> Type) -> Name -> [Type] -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Type
    hsVar (Name -> [Type] -> Type)
    -> ExceptT WhyNotAHaskellType HsCompileM Name
    -> ExceptT WhyNotAHaskellType HsCompileM ([Type] -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> ExceptT WhyNotAHaskellType HsCompileM Name
    forall (tcm :: * -> *).
    (MonadDebug tcm, MonadTCM tcm) =>
    Int -> tcm Name
    getHsVar Int
    x ExceptT WhyNotAHaskellType HsCompileM ([Type] -> Type)
    -> ExceptT WhyNotAHaskellType HsCompileM [Type] -> ToHs Type
    forall a b.
    ExceptT WhyNotAHaskellType HsCompileM (a -> b)
    -> ExceptT WhyNotAHaskellType HsCompileM a
    -> ExceptT WhyNotAHaskellType HsCompileM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Arg Term] -> ExceptT WhyNotAHaskellType HsCompileM [Type]
    fromArgs [Arg Term]
    args
            Def QName
    d Elims
    es -> do
              let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
              Type -> [Type] -> Type
    hsApp (Type -> [Type] -> Type)
    -> ToHs Type
    -> ExceptT WhyNotAHaskellType HsCompileM ([Type] -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> ToHs Type
    getHsType QName
    d ExceptT WhyNotAHaskellType HsCompileM ([Type] -> Type)
    -> ExceptT WhyNotAHaskellType HsCompileM [Type] -> ToHs Type
    forall a b.
    ExceptT WhyNotAHaskellType HsCompileM (a -> b)
    -> ExceptT WhyNotAHaskellType HsCompileM a
    -> ExceptT WhyNotAHaskellType HsCompileM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Arg Term] -> ExceptT WhyNotAHaskellType HsCompileM [Type]
    fromArgs [Arg Term]
    args
            Pi Dom Type
    a Abs Type
    b ->
              if Abs Type -> Bool
    forall a. Free a => Abs a -> Bool
    isBinderUsed Abs Type
    b  -- Andreas, 2012-04-03.  Q: could we rely on Abs/NoAbs instead of again checking freeness of variable?
              then do
                hsA <- Type -> ToHs Type
    fromType (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a)
                liftE1' (underAbstraction a b) $ \ Type
    b ->
                  Name -> Type -> Type
    hsForall (Name -> Type -> Type)
    -> ExceptT WhyNotAHaskellType HsCompileM Name
    -> ExceptT WhyNotAHaskellType HsCompileM (Type -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> ExceptT WhyNotAHaskellType HsCompileM Name
    forall (tcm :: * -> *).
    (MonadDebug tcm, MonadTCM tcm) =>
    Int -> tcm Name
    getHsVar Int
    0 ExceptT WhyNotAHaskellType HsCompileM (Type -> Type)
    -> ToHs Type -> ToHs Type
    forall a b.
    ExceptT WhyNotAHaskellType HsCompileM (a -> b)
    -> ExceptT WhyNotAHaskellType HsCompileM a
    -> ExceptT WhyNotAHaskellType HsCompileM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Type -> Type -> Type
    hsFun Type
    hsA (Type -> Type) -> ToHs Type -> ToHs Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> ToHs Type
    fromType Type
    b)
              else Type -> Type -> Type
    hsFun (Type -> Type -> Type)
    -> ToHs Type
    -> ExceptT WhyNotAHaskellType HsCompileM (Type -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> ToHs Type
    fromType (Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) ExceptT WhyNotAHaskellType HsCompileM (Type -> Type)
    -> ToHs Type -> ToHs Type
    forall a b.
    ExceptT WhyNotAHaskellType HsCompileM (a -> b)
    -> ExceptT WhyNotAHaskellType HsCompileM a
    -> ExceptT WhyNotAHaskellType HsCompileM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Type -> ToHs Type
    fromType (Impossible -> Abs Type -> Type
    forall a. Subst a => Impossible -> Abs a -> a
    noabsApp Impossible
    forall a. HasCallStack => a
    __IMPOSSIBLE__ Abs Type
    b)
            Con ConHead
    c ConInfo
    ci Elims
    es -> do
              let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
              Type -> [Type] -> Type
    hsApp (Type -> [Type] -> Type)
    -> ToHs Type
    -> ExceptT WhyNotAHaskellType HsCompileM ([Type] -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> ToHs Type
    getHsType (ConHead -> QName
    conName ConHead
    c) ExceptT WhyNotAHaskellType HsCompileM ([Type] -> Type)
    -> ExceptT WhyNotAHaskellType HsCompileM [Type] -> ToHs Type
    forall a b.
    ExceptT WhyNotAHaskellType HsCompileM (a -> b)
    -> ExceptT WhyNotAHaskellType HsCompileM a
    -> ExceptT WhyNotAHaskellType HsCompileM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> [Arg Term] -> ExceptT WhyNotAHaskellType HsCompileM [Type]
    fromArgs [Arg Term]
    args
            Lam{}      -> WhyNotAHaskellType -> ToHs Type
    forall a.
    WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Term -> WhyNotAHaskellType
    BadLambda Term
    v)
            Level{}    -> Type -> ToHs Type
    forall a. a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    hsUnit
            Lit{}      -> Type -> ToHs Type
    forall a. a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    hsUnit
            Sort{}     -> Type -> ToHs Type
    forall a. a -> ExceptT WhyNotAHaskellType HsCompileM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    hsUnit
            MetaV{}    -> WhyNotAHaskellType -> ToHs Type
    forall a.
    WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Term -> WhyNotAHaskellType
    BadMeta Term
    v)
            DontCare{} -> WhyNotAHaskellType -> ToHs Type
    forall a.
    WhyNotAHaskellType -> ExceptT WhyNotAHaskellType HsCompileM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (Term -> WhyNotAHaskellType
    BadDontCare Term
    v)
            Dummy String
    s Elims
    _  -> String -> ToHs Type
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    s

    haskellType :: QName -> HsCompileM HS.Type
    haskellType :: QName -> HsCompileM Type
    haskellType QName
    q = do
      def <- QName
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState (TCMT IO)) Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      let (np, erased) =
            case theDef def of
              Constructor{ Int
    conPars :: Int
    conPars :: Defn -> Int
    conPars, Maybe [Bool]
    conErased :: Maybe [Bool]
    conErased :: Defn -> Maybe [Bool]
    conErased }
                -> (Int
    conPars, [Bool] -> Maybe [Bool] -> [Bool]
    forall a. a -> Maybe a -> a
    fromMaybe [] Maybe [Bool]
    conErased [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    False)
              Defn
    _ -> (Int
    0, Bool -> [Bool]
    forall a. a -> [a]
    repeat Bool
    False)
          stripErased (Bool
    True  : [Bool]
    es) (HS.TyFun Type
    _ Type
    t)     = [Bool] -> Type -> Type
    stripErased [Bool]
    es Type
    t
          stripErased (Bool
    False : [Bool]
    es) (HS.TyFun Type
    s Type
    t)     = Type -> Type -> Type
    HS.TyFun Type
    s (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ [Bool] -> Type -> Type
    stripErased [Bool]
    es Type
    t
          stripErased [Bool]
    es           (HS.TyForall [TyVarBind]
    xs Type
    t) = [TyVarBind] -> Type -> Type
    HS.TyForall [TyVarBind]
    xs (Type -> Type) -> Type -> Type
    forall a b. (a -> b) -> a -> b
    $ [Bool] -> Type -> Type
    stripErased [Bool]
    es Type
    t
          stripErased [Bool]
    _            Type
    t                  = Type
    t
          underPars Int
    0 Type
    a = [Bool] -> Type -> Type
    stripErased [Bool]
    erased (Type -> Type) -> HsCompileM Type -> HsCompileM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Type -> HsCompileM Type
    haskellType' Type
    a
          underPars Int
    n Type
    a = do
            a <- Type -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Type
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Type
    a
            case unEl a of
              Pi Dom Type
    a (NoAbs String
    _ Type
    b) -> Int -> Type -> HsCompileM Type
    underPars (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Type
    b
              Pi Dom Type
    a Abs Type
    b  -> Dom Type
    -> Abs Type -> (Type -> HsCompileM Type) -> HsCompileM Type
    forall a (m :: * -> *) b.
    (Subst a, MonadAddContext m) =>
    Dom Type -> Abs a -> (a -> m b) -> m b
    underAbstraction Dom Type
    a Abs Type
    b ((Type -> HsCompileM Type) -> HsCompileM Type)
    -> (Type -> HsCompileM Type) -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ \Type
    b -> Name -> Type -> Type
    hsForall (Name -> Type -> Type)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Name
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Name
    forall (tcm :: * -> *).
    (MonadDebug tcm, MonadTCM tcm) =>
    Int -> tcm Name
    getHsVar Int
    0 ReaderT
      GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
    -> HsCompileM Type -> HsCompileM Type
    forall a b.
    ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) (a -> b)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int -> Type -> HsCompileM Type
    underPars (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1) Type
    b
              Term
    _       -> HsCompileM Type
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      ty <- underPars np $ defType def
      reportSDoc "tc.pragma.compile" 10 $ (("Haskell type for" <+> prettyTCM q) <> ":") <?> pretty ty
      return ty

    -- Type approximations ----------------------------------------------------

    data PolyApprox = PolyApprox | NoPolyApprox
      deriving (PolyApprox -> PolyApprox -> Bool
    (PolyApprox -> PolyApprox -> Bool)
    -> (PolyApprox -> PolyApprox -> Bool) -> Eq PolyApprox
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PolyApprox -> PolyApprox -> Bool
    == :: PolyApprox -> PolyApprox -> Bool
    $c/= :: PolyApprox -> PolyApprox -> Bool
    /= :: PolyApprox -> PolyApprox -> Bool
    Eq)

    hsTypeApproximation :: PolyApprox -> Int -> Type -> HsCompileM HS.Type
    hsTypeApproximation :: PolyApprox -> Int -> Type -> HsCompileM Type
    hsTypeApproximation PolyApprox
    poly Int
    fv Type
    t = do
      env <- ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) GHCEnv
    forall (m :: * -> *). ReadGHCModuleEnv m => m GHCEnv
    askGHCEnv
      let is QName
    q GHCEnv -> Maybe QName
    b = QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == GHCEnv -> Maybe QName
    b GHCEnv
    env
          tyCon  = QName -> Type
    HS.TyCon (QName -> Type) -> (String -> QName) -> String -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> QName
    HS.UnQual (Name -> QName) -> (String -> Name) -> String -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Name
    HS.Ident
          rteCon = QName -> Type
    HS.TyCon (QName -> Type) -> (String -> QName) -> String -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> Name -> QName
    HS.Qual ModuleName
    mazRTE (Name -> QName) -> (String -> Name) -> String -> QName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Name
    HS.Ident
          tyVar a
    n a
    i = Name -> Type
    HS.TyVar (Name -> Type) -> Name -> Type
    forall a b. (a -> b) -> a -> b
    $ String -> Name
    HS.Ident (String -> Name) -> String -> Name
    forall a b. (a -> b) -> a -> b
    $ String
    "a" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ a -> String
    forall a. Show a => a -> String
    show (a
    n a -> a -> a
    forall a. Num a => a -> a -> a
    - a
    i)
      let go Int
    n Term
    t = do
            String
    -> Int
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "compile.haskell.type" Int
    25 (TCMT IO Doc
     -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ())
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "hsTypeApproximation " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => Term -> m Doc
    prettyTCM Term
    t
            String
    -> Int
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "compile.haskell.type" Int
    50 (TCMT IO Doc
     -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ())
    -> TCMT IO Doc
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "hsTypeApproximation " TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Term -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty Term
    t
            t <- Term -> Term
    unSpine (Term -> Term)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Term
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Term
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Term -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Term
    forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
    reduce Term
    t
            case t of
              Var Int
    i Elims
    _ | PolyApprox
    poly PolyApprox -> PolyApprox -> Bool
    forall a. Eq a => a -> a -> Bool
    == PolyApprox
    PolyApprox -> Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ Int -> Int -> Type
    forall {a}. (Show a, Num a) => a -> a -> Type
    tyVar Int
    n Int
    i
              Pi Dom Type
    a Abs Type
    b -> Type -> Type -> Type
    hsFun (Type -> Type -> Type)
    -> HsCompileM Type
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Term -> HsCompileM Type
    go Int
    n (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Dom Type -> Type
    forall t e. Dom' t e -> e
    unDom Dom Type
    a) ReaderT
      GHCModuleEnv (StateT HsCompileState (TCMT IO)) (Type -> Type)
    -> HsCompileM Type -> HsCompileM Type
    forall a b.
    ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) (a -> b)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Int -> Term -> HsCompileM Type
    go (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    k) (Type -> Term
    forall t a. Type'' t a -> a
    unEl (Type -> Term) -> Type -> Term
    forall a b. (a -> b) -> a -> b
    $ Abs Type -> Type
    forall a. Abs a -> a
    unAbs Abs Type
    b)
                where k :: Int
    k = case Abs Type
    b of Abs{} -> Int
    1; NoAbs{} -> Int
    0
              Def QName
    q Elims
    els
                | QName
    q QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvList
                , Just Int
    k <- GHCEnv -> Maybe Int
    ghcEnvListArity GHCEnv
    env
                , [Apply Arg Term
    t] <- Int -> Elims -> Elims
    forall a. Int -> [a] -> [a]
    drop (Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Elims
    els ->
                  Type -> Type -> Type
    HS.TyApp (String -> Type
    tyCon String
    "[]") (Type -> Type) -> HsCompileM Type -> HsCompileM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Term -> HsCompileM Type
    go Int
    n (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t)
                | QName
    q QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvMaybe
                , Just Int
    k <- GHCEnv -> Maybe Int
    ghcEnvMaybeArity GHCEnv
    env
                , [Apply Arg Term
    t] <- Int -> Elims -> Elims
    forall a. Int -> [a] -> [a]
    drop (Int
    kInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1) Elims
    els ->
                  Type -> Type -> Type
    HS.TyApp (String -> Type
    tyCon String
    "Maybe") (Type -> Type) -> HsCompileM Type -> HsCompileM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> Term -> HsCompileM Type
    go Int
    n (Arg Term -> Term
    forall e. Arg e -> e
    unArg Arg Term
    t)
                | QName
    q QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvBool    -> Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    tyCon String
    "Bool"
                | QName
    q QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvInteger -> Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    tyCon String
    "Integer"
                | QName
    q QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvNat     -> Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    tyCon String
    "Integer"
                | QName
    q QName -> (GHCEnv -> Maybe QName) -> Bool
    `is` GHCEnv -> Maybe QName
    ghcEnvWord64  -> Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    rteCon String
    "Word64"
                | Bool
    otherwise -> do
                    let args :: [Arg Term]
    args = [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
    forall a. a -> Maybe a -> a
    fromMaybe [Arg Term]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe [Arg Term]
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    els
                    (Type -> Type -> Type) -> Type -> [Type] -> Type
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Type -> Type -> Type
    HS.TyApp (Type -> [Type] -> Type)
    -> HsCompileM Type
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState (TCMT IO)) ([Type] -> Type)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> HsCompileM Type
    getHsType' QName
    q ReaderT
      GHCModuleEnv (StateT HsCompileState (TCMT IO)) ([Type] -> Type)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) [Type]
    -> HsCompileM Type
    forall a b.
    ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) (a -> b)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (Arg Term -> HsCompileM Type)
    -> [Arg Term]
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) [Type]
    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 (Int -> Term -> HsCompileM Type
    go Int
    n (Term -> HsCompileM Type)
    -> (Arg Term -> Term) -> Arg Term -> HsCompileM Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Arg Term -> Term
    forall e. Arg e -> e
    unArg) [Arg Term]
    args
                  HsCompileM Type -> (TCErr -> HsCompileM Type) -> HsCompileM Type
    forall a.
    ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    -> (TCErr
        -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall e (m :: * -> *) a.
    MonadError e m =>
    m a -> (e -> m a) -> m a
    `catchError` \ TCErr
    _ -> -- Not a Haskell type
                    ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
    -> HsCompileM Type -> HsCompileM Type -> HsCompileM Type
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM (ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
    forall (m :: * -> *). Monad m => m Bool -> m Bool -> m Bool
    and2M (QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isCompiled QName
    q) (QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) Bool
    forall (m :: * -> *). HasConstInfo m => QName -> m Bool
    isData QName
    q))
                      (QName -> Type
    HS.TyCon (QName -> Type)
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    -> HsCompileM Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NameKind
    -> QName
    -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) QName
    xhqn NameKind
    TypeK QName
    q)
                      (Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    mazAnyType)
              Sort{} -> Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Type -> HsCompileM Type) -> Type -> HsCompileM Type
    forall a b. (a -> b) -> a -> b
    $ String -> Type
    HS.FakeType String
    "()"
              Term
    _ -> Type -> HsCompileM Type
    forall a.
    a -> ReaderT GHCModuleEnv (StateT HsCompileState (TCMT IO)) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Type
    mazAnyType
      go fv (unEl t)

    -- Approximating polymorphic types is not actually a good idea unless we
    -- actually keep track of type applications in recursive functions, and
    -- generate parameterised datatypes. Otherwise we'll just coerce all type
    -- variables to `Any` at the first `unsafeCoerce`.
    hsTelApproximation :: Type -> HsCompileM ([HS.Type], HS.Type)
    hsTelApproximation :: Type -> HsCompileM ([Type], Type)
    hsTelApproximation = PolyApprox -> Type -> HsCompileM ([Type], Type)
    hsTelApproximation' PolyApprox
    NoPolyApprox

    hsTelApproximation' :: PolyApprox -> Type -> HsCompileM ([HS.Type], HS.Type)
    hsTelApproximation' :: PolyApprox -> Type -> HsCompileM ([Type], Type)
    hsTelApproximation' PolyApprox
    poly Type
    t = do
      TelV tel res <- Type
    -> ReaderT
         GHCModuleEnv (StateT HsCompileState (TCMT IO)) (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
      let args = (Dom' Term (String, Type) -> Type)
    -> [Dom' Term (String, Type)] -> [Type]
    forall a b. (a -> b) -> [a] -> [b]
    map ((String, Type) -> Type
    forall a b. (a, b) -> b
    snd ((String, Type) -> Type)
    -> (Dom' Term (String, Type) -> (String, Type))
    -> Dom' Term (String, Type)
    -> Type
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Dom' Term (String, Type) -> (String, Type)
    forall t e. Dom' t e -> e
    unDom) (Tele (Dom Type) -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Tele (Dom Type)
    tel)
      (,) <$> zipWithM (hsTypeApproximation poly) [0..] args <*> hsTypeApproximation poly (length args) res