-- | 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