{-# LANGUAGE LambdaCase #-}

module Intensional.FromCore
  ( freshCoreType,
    freshCoreScheme,
    fromCoreCons,
    consInstArgs,
    getVar,
  )
where

import Control.Monad.RWS
import qualified Data.IntSet as I
import qualified Data.Map as M
import GhcPlugins hiding ((<>), Expr (..), Type)
import Intensional.InferM
import Intensional.Scheme as Scheme
import ToIface
import qualified TyCoRep as Tcr
import Intensional.Types

-- A fresh monomorphic type
freshCoreType :: Tcr.Type -> InferM Type
freshCoreType :: Type -> InferM Type
freshCoreType = Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
forall a. Maybe a
Nothing

-- A fresh polymorphic type
freshCoreScheme :: Tcr.Type -> InferM Scheme
freshCoreScheme :: Type -> InferM Scheme
freshCoreScheme = Maybe RVar -> Type -> InferM Scheme
fromCoreScheme Maybe RVar
forall a. Maybe a
Nothing

-- The type of a constructor injected into a fresh refinement environment
fromCoreCons :: DataCon -> InferM Scheme
fromCoreCons :: DataCon -> InferM Scheme
fromCoreCons k :: DataCon
k = do
  RVar
x <- InferM RVar
fresh
  let d :: TyCon
d = DataCon -> TyCon
dataConTyCon DataCon
k
  Bool
b <- TyCon -> InferM Bool
isIneligible TyCon
d
  Bool
-> RWST InferEnv ConstraintSet InferState Identity ()
-> RWST InferEnv ConstraintSet InferState Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
b (RWST InferEnv ConstraintSet InferState Identity ()
 -> RWST InferEnv ConstraintSet InferState Identity ())
-> RWST InferEnv ConstraintSet InferState Identity ()
-> RWST InferEnv ConstraintSet InferState Identity ()
forall a b. (a -> b) -> a -> b
$ do
    SrcSpan
l <- (InferEnv -> SrcSpan)
-> RWST InferEnv ConstraintSet InferState Identity SrcSpan
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> SrcSpan
inferLoc
    DataCon
-> SrcSpan
-> DataType TyCon
-> RWST InferEnv ConstraintSet InferState Identity ()
emitKD DataCon
k SrcSpan
l (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
x TyCon
d)
  Maybe RVar -> Type -> InferM Scheme
fromCoreScheme (RVar -> Maybe RVar
forall a. a -> Maybe a
Just RVar
x) (DataCon -> Type
dataConUserType DataCon
k)

-- The argument types of an instantiated constructor
consInstArgs :: RVar -> [Type] -> DataCon -> InferM [Type]
consInstArgs :: RVar -> [Type] -> DataCon -> InferM [Type]
consInstArgs x :: RVar
x as :: [Type]
as k :: DataCon
k = (Type -> InferM Type) -> [Type] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> InferM Type
fromCoreInst (DataCon -> [Type]
dataConRepArgTys DataCon
k)
  where
    fromCoreInst :: Tcr.Type -> InferM Type
    fromCoreInst :: Type -> InferM Type
fromCoreInst (Tcr.TyVarTy a :: Var
a) =
      case Var -> [(Var, Type)] -> Maybe Type
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Var
a ([Var] -> [Type] -> [(Var, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip (DataCon -> [Var]
dataConUnivTyVars DataCon
k) [Type]
as) of
        Nothing -> Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> Type
forall d. Name -> TypeGen d
Var (Var -> Name
forall a. NamedThing a => a -> Name
getName Var
a))
        Just t :: Type
t -> Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
t
    fromCoreInst (Tcr.AppTy a :: Type
a b :: Type
b) = Type -> Type -> Type
forall d. TypeGen d -> TypeGen d -> TypeGen d
App (Type -> Type -> Type)
-> InferM Type
-> RWST InferEnv ConstraintSet InferState Identity (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> InferM Type
fromCoreInst Type
a) RWST InferEnv ConstraintSet InferState Identity (Type -> Type)
-> InferM Type -> InferM Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Type -> InferM Type
fromCoreInst Type
b)
    fromCoreInst (Tcr.TyConApp d :: TyCon
d as' :: [Type]
as')
      | TyCon -> Bool
isTypeSynonymTyCon TyCon
d,
        Just (as'' :: [Var]
as'', s :: Type
s) <- TyCon -> Maybe ([Var], Type)
synTyConDefn_maybe TyCon
d =
        Type -> InferM Type
fromCoreInst (Subst -> Type -> Type
substTy (Subst -> [(Var, Type)] -> Subst
extendTvSubstList Subst
emptySubst ([Var] -> [Type] -> [(Var, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
as'' [Type]
as')) Type
s) -- Instantiate type synonym arguments
      | TyCon -> Bool
isClassTyCon TyCon
d = Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
forall d. TypeGen d
Ambiguous -- Disregard type class evidence
      | Bool
otherwise =
          do  Bool
b <- TyCon -> InferM Bool
isIneligible TyCon
d
              if Bool
b then DataType TyCon -> [Type] -> Type
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (TyCon -> DataType TyCon
forall d. d -> DataType d
Base TyCon
d) ([Type] -> Type) -> InferM [Type] -> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type -> InferM Type) -> [Type] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> InferM Type
fromCoreInst [Type]
as') 
                   else DataType TyCon -> [Type] -> Type
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
x TyCon
d) ([Type] -> Type) -> InferM [Type] -> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Type -> InferM Type) -> [Type] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> InferM Type
fromCoreInst [Type]
as')
    fromCoreInst (Tcr.FunTy a :: Type
a b :: Type
b) = Type -> Type -> Type
forall d. TypeGen d -> TypeGen d -> TypeGen d
(:=>) (Type -> Type -> Type)
-> InferM Type
-> RWST InferEnv ConstraintSet InferState Identity (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> InferM Type
fromCoreInst Type
a RWST InferEnv ConstraintSet InferState Identity (Type -> Type)
-> InferM Type -> InferM Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> InferM Type
fromCoreInst Type
b
    fromCoreInst (Tcr.LitTy l :: TyLit
l) = Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (IfaceTyLit -> Type
forall d. IfaceTyLit -> TypeGen d
Lit (IfaceTyLit -> Type) -> IfaceTyLit -> Type
forall a b. (a -> b) -> a -> b
$ TyLit -> IfaceTyLit
toIfaceTyLit TyLit
l)
    fromCoreInst _ = Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
forall d. TypeGen d
Ambiguous

-- Convert a monomorphic core type
fromCore :: Maybe RVar -> Tcr.Type -> InferM Type
fromCore :: Maybe RVar -> Type -> InferM Type
fromCore _ (Tcr.TyVarTy a :: Var
a) = Name -> Type
forall d. Name -> TypeGen d
Var (Name -> Type)
-> RWST InferEnv ConstraintSet InferState Identity Name
-> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Var -> RWST InferEnv ConstraintSet InferState Identity Name
forall a.
NamedThing a =>
a -> RWST InferEnv ConstraintSet InferState Identity Name
getExternalName Var
a
fromCore f :: Maybe RVar
f (Tcr.AppTy a :: Type
a b :: Type
b) = (Type -> Type -> Type) -> InferM Type -> InferM Type -> InferM Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
forall d. TypeGen d -> TypeGen d -> TypeGen d
App (Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
f Type
a) (Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
f Type
b)
fromCore f :: Maybe RVar
f (Tcr.TyConApp d :: TyCon
d as :: [Type]
as)
  | TyCon -> Bool
isTypeSynonymTyCon TyCon
d,
    Just (as' :: [Var]
as', s :: Type
s) <- TyCon -> Maybe ([Var], Type)
synTyConDefn_maybe TyCon
d =
    Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
f (Subst -> Type -> Type
substTy (Subst -> [(Var, Type)] -> Subst
extendTvSubstList Subst
emptySubst ([Var] -> [Type] -> [(Var, Type)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Var]
as' [Type]
as)) Type
s) -- Instantiate type synonyms
  | TyCon -> Bool
isClassTyCon TyCon
d = Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
forall d. TypeGen d
Ambiguous -- Disregard type class evidence
fromCore Nothing (Tcr.TyConApp d :: TyCon
d as :: [Type]
as) = do
  RVar
x <- InferM RVar
fresh
  Bool
b <- TyCon -> InferM Bool
isIneligible TyCon
d
  if Bool
b then
    DataType TyCon -> [Type] -> Type
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (TyCon -> DataType TyCon
forall d. d -> DataType d
Base TyCon
d) ([Type] -> Type) -> InferM [Type] -> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> InferM Type) -> [Type] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
forall a. Maybe a
Nothing) [Type]
as
  else
    DataType TyCon -> [Type] -> Type
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
x TyCon
d) ([Type] -> Type) -> InferM [Type] -> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> InferM Type) -> [Type] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
forall a. Maybe a
Nothing) [Type]
as
fromCore (Just x :: RVar
x) (Tcr.TyConApp d :: TyCon
d as :: [Type]
as) = do
  Bool
b <- TyCon -> InferM Bool
isIneligible TyCon
d
  if Bool
b then
    DataType TyCon -> [Type] -> Type
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (TyCon -> DataType TyCon
forall d. d -> DataType d
Base TyCon
d) ([Type] -> Type) -> InferM [Type] -> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> InferM Type) -> [Type] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe RVar -> Type -> InferM Type
fromCore (RVar -> Maybe RVar
forall a. a -> Maybe a
Just RVar
x)) [Type]
as
  else
    DataType TyCon -> [Type] -> Type
forall d. DataType d -> [TypeGen d] -> TypeGen d
Data (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
x TyCon
d) ([Type] -> Type) -> InferM [Type] -> InferM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Type -> InferM Type) -> [Type] -> InferM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Maybe RVar -> Type -> InferM Type
fromCore (RVar -> Maybe RVar
forall a. a -> Maybe a
Just RVar
x)) [Type]
as
fromCore f :: Maybe RVar
f (Tcr.FunTy a :: Type
a b :: Type
b) = (Type -> Type -> Type) -> InferM Type -> InferM Type -> InferM Type
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Type -> Type -> Type
forall d. TypeGen d -> TypeGen d -> TypeGen d
(:=>) (Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
f Type
a) (Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
f Type
b)
fromCore _ (Tcr.LitTy l :: TyLit
l) = Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> InferM Type) -> Type -> InferM Type
forall a b. (a -> b) -> a -> b
$ IfaceTyLit -> Type
forall d. IfaceTyLit -> TypeGen d
Lit (IfaceTyLit -> Type) -> IfaceTyLit -> Type
forall a b. (a -> b) -> a -> b
$ TyLit -> IfaceTyLit
toIfaceTyLit TyLit
l
fromCore _ _ = Type -> InferM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
forall d. TypeGen d
Ambiguous -- Higher-ranked or impredicative types, casts and coercions

-- Convert a polymorphic core type
fromCoreScheme :: Maybe RVar -> Tcr.Type -> InferM Scheme
fromCoreScheme :: Maybe RVar -> Type -> InferM Scheme
fromCoreScheme f :: Maybe RVar
f (Tcr.ForAllTy b :: TyCoVarBinder
b t :: Type
t) = do
  Name
a <- Var -> RWST InferEnv ConstraintSet InferState Identity Name
forall a.
NamedThing a =>
a -> RWST InferEnv ConstraintSet InferState Identity Name
getExternalName (TyCoVarBinder -> Var
forall tv argf. VarBndr tv argf -> tv
Tcr.binderVar TyCoVarBinder
b)
  Scheme
scheme <- Maybe RVar -> Type -> InferM Scheme
fromCoreScheme Maybe RVar
f Type
t
  Scheme -> InferM Scheme
forall (m :: * -> *) a. Monad m => a -> m a
return Scheme
scheme {tyvars :: [Name]
tyvars = Name
a Name -> [Name] -> [Name]
forall a. a -> [a] -> [a]
: Scheme -> [Name]
forall d. SchemeGen d -> [Name]
tyvars Scheme
scheme}
fromCoreScheme f :: Maybe RVar
f (Tcr.FunTy a :: Type
a b :: Type
b) = do
  Type
a' <- Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
f Type
a
  Scheme
scheme <- Maybe RVar -> Type -> InferM Scheme
fromCoreScheme Maybe RVar
f Type
b -- Optimistically push arrows inside univiersal quantifier
  Scheme -> InferM Scheme
forall (m :: * -> *) a. Monad m => a -> m a
return Scheme
scheme {body :: Type
body = Type
a' Type -> Type -> Type
forall d. TypeGen d -> TypeGen d -> TypeGen d
:=> Scheme -> Type
forall d. SchemeGen d -> TypeGen d
body Scheme
scheme}
fromCoreScheme f :: Maybe RVar
f t :: Type
t = [Name] -> Type -> Scheme
forall d. [Name] -> TypeGen d -> SchemeGen d
Forall [] (Type -> Scheme) -> InferM Type -> InferM Scheme
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe RVar -> Type -> InferM Type
fromCore Maybe RVar
f Type
t

-- Lookup constrained variable and emit its constraints
getVar :: Var -> InferM Scheme
getVar :: Var -> InferM Scheme
getVar v :: Var
v =
  (InferEnv -> Maybe Scheme)
-> RWST InferEnv ConstraintSet InferState Identity (Maybe Scheme)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks (Name -> Map Name Scheme -> Maybe Scheme
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Var -> Name
forall a. NamedThing a => a -> Name
getName Var
v) (Map Name Scheme -> Maybe Scheme)
-> (InferEnv -> Map Name Scheme) -> InferEnv -> Maybe Scheme
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InferEnv -> Map Name Scheme
varEnv) RWST InferEnv ConstraintSet InferState Identity (Maybe Scheme)
-> (Maybe Scheme -> InferM Scheme) -> InferM Scheme
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just scheme :: Scheme
scheme -> do
      -- Localise constraints
      Scheme
fre_scheme <-
        (Scheme -> RVar -> InferM Scheme)
-> Scheme -> [RVar] -> InferM Scheme
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          ( \s :: Scheme
s x :: RVar
x -> do
              RVar
y <- InferM RVar
fresh
              Scheme -> InferM Scheme
forall (m :: * -> *) a. Monad m => a -> m a
return (RVar -> RVar -> Scheme -> Scheme
forall t. Refined t => RVar -> RVar -> t -> t
rename RVar
x RVar
y Scheme
s)
          )
          (Scheme
scheme {boundvs :: Domain
boundvs = Domain
forall a. Monoid a => a
mempty})
          (Domain -> [RVar]
I.toList (Scheme -> Domain
forall d. SchemeGen d -> Domain
boundvs Scheme
scheme))
      -- Emit constriants associated with a variable
      ConstraintSet -> RWST InferEnv ConstraintSet InferState Identity ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (Scheme -> ConstraintSet
forall d. SchemeGen d -> ConstraintSet
constraints Scheme
fre_scheme)
      Scheme -> InferM Scheme
forall (m :: * -> *) a. Monad m => a -> m a
return Scheme
fre_scheme {constraints :: ConstraintSet
Scheme.constraints = ConstraintSet
forall a. Monoid a => a
mempty}
    Nothing -> do
      Scheme
var_scheme <- Type -> InferM Scheme
freshCoreScheme (Type -> InferM Scheme) -> Type -> InferM Scheme
forall a b. (a -> b) -> a -> b
$ Var -> Type
varType Var
v
      Bool -> Type -> RWST InferEnv ConstraintSet InferState Identity ()
maximise Bool
True (Scheme -> Type
forall d. SchemeGen d -> TypeGen d
body Scheme
var_scheme)
      Scheme -> InferM Scheme
forall (m :: * -> *) a. Monad m => a -> m a
return Scheme
var_scheme

-- Maximise/minimise a library type, i.e. assert every constructor occurs in covariant positions
maximise :: Bool -> Type -> InferM ()
maximise :: Bool -> Type -> RWST InferEnv ConstraintSet InferState Identity ()
maximise True (Data (Inj x :: RVar
x d :: TyCon
d) _) = do
  SrcSpan
l <- (InferEnv -> SrcSpan)
-> RWST InferEnv ConstraintSet InferState Identity SrcSpan
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks InferEnv -> SrcSpan
inferLoc
  (DataCon -> RWST InferEnv ConstraintSet InferState Identity ())
-> [DataCon] -> RWST InferEnv ConstraintSet InferState Identity ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\k :: DataCon
k -> DataCon
-> SrcSpan
-> DataType TyCon
-> RWST InferEnv ConstraintSet InferState Identity ()
emitKD DataCon
k SrcSpan
l (RVar -> TyCon -> DataType TyCon
forall d. RVar -> d -> DataType d
Inj RVar
x TyCon
d)) ([DataCon] -> RWST InferEnv ConstraintSet InferState Identity ())
-> [DataCon] -> RWST InferEnv ConstraintSet InferState Identity ()
forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
d
maximise b :: Bool
b (x :: Type
x :=> y :: Type
y) = Bool -> Type -> RWST InferEnv ConstraintSet InferState Identity ()
maximise (Bool -> Bool
not Bool
b) Type
x RWST InferEnv ConstraintSet InferState Identity ()
-> RWST InferEnv ConstraintSet InferState Identity ()
-> RWST InferEnv ConstraintSet InferState Identity ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> Type -> RWST InferEnv ConstraintSet InferState Identity ()
maximise Bool
b Type
y
maximise _ _ = () -> RWST InferEnv ConstraintSet InferState Identity ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()