{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE CPP #-}

-- | This module implements the check that the transformed code is
-- typable in the single tick calculus.

module Rattus.Plugin.CheckSingleTick
  (checkExpr, CheckExpr (..)) where

#if __GLASGOW_HASKELL__ >= 902
import GHC.Types.Tickish
#endif


#if __GLASGOW_HASKELL__ >= 900
import GHC.Plugins
#else
import GhcPlugins
#endif

import Rattus.Plugin.Utils 

import Prelude hiding ((<>))
import Control.Monad
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Control.Applicative
import Data.Foldable

type LCtx = Set Var
data HiddenReason = BoxApp | AdvApp | NestedRec Var | FunDef | DelayApp
type Hidden = Map Var HiddenReason

data Prim = Delay | Adv | Box | Arr

data TypeError = TypeError SrcSpan SDoc

instance Outputable Prim where
  ppr :: Prim -> SDoc
ppr Prim
Delay = SDoc
"delay"
  ppr Prim
Adv = SDoc
"adv"
  ppr Prim
Box = SDoc
"box"
  ppr Prim
Arr = SDoc
"arr"
  
data Ctx = Ctx
  { Ctx -> LCtx
current :: LCtx,
    Ctx -> Hidden
hidden :: Hidden,
    Ctx -> Maybe LCtx
earlier :: Maybe LCtx,
    Ctx -> SrcSpan
srcLoc :: SrcSpan,
    Ctx -> LCtx
recDef :: Set Var, -- ^ recursively defined variables 
    Ctx -> LCtx
stableTypes :: Set Var,
    Ctx -> Map Var Prim
primAlias :: Map Var Prim,
    -- number of ticks (for recursive calls). This is to allow
    -- recursive definitions of the form @f = delay (delay (adv f))@.
    Ctx -> Int
ticks :: Int,
    Ctx -> Bool
allowRecursion :: Bool} 

primMap :: Map FastString Prim
primMap :: Map FastString Prim
primMap = forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
  [(FastString
"delay", Prim
Delay),
   (FastString
"adv", Prim
Adv),
   (FastString
"box", Prim
Box),
   (FastString
"arr", Prim
Arr)
   ]


isPrim :: Ctx -> Var -> Maybe Prim
isPrim :: Ctx -> Var -> Maybe Prim
isPrim Ctx
c Var
v
  | Just Prim
p <- forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v (Ctx -> Map Var Prim
primAlias Ctx
c) = forall a. a -> Maybe a
Just Prim
p
  | Bool
otherwise = do
  (FastString
name,FastString
mod) <- forall a. NamedThing a => a -> Maybe (FastString, FastString)
getNameModule Var
v
  if FastString -> Bool
isRattModule FastString
mod then forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup FastString
name Map FastString Prim
primMap
  else forall a. Maybe a
Nothing



stabilize :: HiddenReason -> Ctx -> Ctx
stabilize :: HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
hr Ctx
c = Ctx
c
  {current :: LCtx
current = forall a. Set a
Set.empty,
   earlier :: Maybe LCtx
earlier = forall a. Maybe a
Nothing,
   hidden :: Hidden
hidden = Ctx -> Hidden
hidden Ctx
c forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const HiddenReason
hr) LCtx
ctxHid,
   ticks :: Int
ticks = Int
0}
  where ctxHid :: LCtx
ctxHid = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ctx -> LCtx
current Ctx
c) (forall a. Ord a => Set a -> Set a -> Set a
Set.union (Ctx -> LCtx
current Ctx
c)) (Ctx -> Maybe LCtx
earlier Ctx
c)


data Scope = Hidden SDoc | Visible

getScope  :: Ctx -> Var -> Scope
getScope :: Ctx -> Var -> Scope
getScope Ctx
c Var
v =
    if Var
v forall a. Ord a => a -> Set a -> Bool
`Set.member` Ctx -> LCtx
recDef Ctx
c then
      if Ctx -> Int
ticks Ctx
c forall a. Ord a => a -> a -> Bool
> Int
0 Bool -> Bool -> Bool
|| Ctx -> Bool
allowRecursion Ctx
c then Scope
Visible
      else SDoc -> Scope
Hidden (SDoc
"(Mutually) recursive call to " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" must occur under delay")
    else case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Var
v (Ctx -> Hidden
hidden Ctx
c) of
      Just HiddenReason
reason ->
        if (LCtx -> Kind -> Bool
isStable (Ctx -> LCtx
stableTypes Ctx
c) (Var -> Kind
varType Var
v)) then Scope
Visible
        else case HiddenReason
reason of
          NestedRec Var
rv ->
            if Ctx -> Bool
allowRecursion Ctx
c then Scope
Visible
            else SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope:"
                         SDoc -> SDoc -> SDoc
$$ SDoc
"It appears in a local recursive definition (namely of " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
rv SDoc -> SDoc -> SDoc
<> SDoc
")"
                         SDoc -> SDoc -> SDoc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", which is not stable.")
          HiddenReason
BoxApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope:" SDoc -> SDoc -> SDoc
$$
                       SDoc
"It occurs under " SDoc -> SDoc -> SDoc
<> SDoc -> SDoc
keyword SDoc
"box" SDoc -> SDoc -> SDoc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", which is not stable.")
          HiddenReason
AdvApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope: It occurs under adv.")
        
          HiddenReason
FunDef -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope: It occurs in a function that is defined under a delay, is a of a non-stable type " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", and is bound outside delay")
          HiddenReason
DelayApp -> SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope: It occurs under two occurrences of delay and is a of a non-stable type " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v))
      Maybe HiddenReason
Nothing
          | forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall a. Ord a => a -> Set a -> Bool
Set.member Var
v) (Ctx -> Maybe LCtx
earlier Ctx
c) ->
            if LCtx -> Kind -> Bool
isStable (Ctx -> LCtx
stableTypes Ctx
c) (Var -> Kind
varType Var
v) then Scope
Visible
            else SDoc -> Scope
Hidden (SDoc
"Variable " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr Var
v SDoc -> SDoc -> SDoc
<> SDoc
" is no longer in scope:" SDoc -> SDoc -> SDoc
$$
                         SDoc
"It occurs under delay" SDoc -> SDoc -> SDoc
$$ SDoc
"and is of type " SDoc -> SDoc -> SDoc
<> forall a. Outputable a => a -> SDoc
ppr (Var -> Kind
varType Var
v) SDoc -> SDoc -> SDoc
<> SDoc
", which is not stable.")
          | forall a. Ord a => a -> Set a -> Bool
Set.member Var
v (Ctx -> LCtx
current Ctx
c) -> Scope
Visible
          | Bool
otherwise -> Scope
Visible



pickFirst :: SrcSpan -> SrcSpan -> SrcSpan
pickFirst :: SrcSpan -> SrcSpan -> SrcSpan
pickFirst s :: SrcSpan
s@RealSrcSpan{} SrcSpan
_ = SrcSpan
s
pickFirst SrcSpan
_ SrcSpan
s = SrcSpan
s


typeError :: Ctx -> Var -> SDoc -> CoreM (Maybe TypeError)
typeError :: Ctx -> Var -> SDoc -> CoreM (Maybe TypeError)
typeError Ctx
cxt Var
var SDoc
doc =
  forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (SrcSpan -> SDoc -> TypeError
TypeError (SrcSpan -> SrcSpan -> SrcSpan
pickFirst (Ctx -> SrcSpan
srcLoc Ctx
cxt) (Name -> SrcSpan
nameSrcSpan (Var -> Name
varName Var
var))) SDoc
doc))


emptyCtx :: CheckExpr -> Ctx
emptyCtx :: CheckExpr -> Ctx
emptyCtx CheckExpr
c =
  Ctx { current :: LCtx
current =  forall a. Set a
Set.empty,
        earlier :: Maybe LCtx
earlier = forall a. Maybe a
Nothing,
        hidden :: Hidden
hidden = forall k a. Map k a
Map.empty,
        srcLoc :: SrcSpan
srcLoc = SrcSpan
noLocationInfo,
        recDef :: LCtx
recDef = CheckExpr -> LCtx
recursiveSet CheckExpr
c,
        primAlias :: Map Var Prim
primAlias = forall k a. Map k a
Map.empty,
        stableTypes :: LCtx
stableTypes = forall a. Set a
Set.empty,
        ticks :: Int
ticks = Int
0,
        allowRecursion :: Bool
allowRecursion = CheckExpr -> Bool
allowRecExp CheckExpr
c}


isPrimExpr :: Ctx -> Expr Var -> Maybe (Prim,Var)
isPrimExpr :: Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c (App Expr Var
e (Type Kind
_)) = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr Ctx
c (App Expr Var
e Expr Var
e') | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Kind -> Bool
tcIsLiftedTypeKind forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Kind -> Kind
typeKind forall a b. (a -> b) -> a -> b
$ Expr Var -> Kind
exprType Expr Var
e' = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr Ctx
c (Var Var
v) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (,Var
v) (Ctx -> Var -> Maybe Prim
isPrim Ctx
c Var
v)
isPrimExpr Ctx
c (Tick CoreTickish
_ Expr Var
e) = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr Ctx
c (Lam Var
v Expr Var
e)
  | Var -> Bool
isTyVar Var
v Bool -> Bool -> Bool
|| (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Kind -> Bool
tcIsLiftedTypeKind forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Kind -> Kind
typeKind forall a b. (a -> b) -> a -> b
$ Var -> Kind
varType Var
v) = Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e
isPrimExpr Ctx
_ Expr Var
_ = forall a. Maybe a
Nothing


stabilizeLater :: Ctx -> Ctx
stabilizeLater :: Ctx -> Ctx
stabilizeLater Ctx
c =
  case Ctx -> Maybe LCtx
earlier Ctx
c of
    Just LCtx
earl -> Ctx
c {earlier :: Maybe LCtx
earlier = forall a. Maybe a
Nothing,
                    hidden :: Hidden
hidden = Ctx -> Hidden
hidden Ctx
c forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const HiddenReason
FunDef) LCtx
earl}
    Maybe LCtx
Nothing -> Ctx
c 

isStableConstr :: Type -> CoreM (Maybe Var)
isStableConstr :: Kind -> CoreM (Maybe Var)
isStableConstr Kind
t = 
  case HasDebugCallStack => Kind -> Maybe (TyCon, [Kind])
splitTyConApp_maybe Kind
t of
    Just (TyCon
con,[Kind
args]) ->
      case forall a. NamedThing a => a -> Maybe (FastString, FastString)
getNameModule TyCon
con of
        Just (FastString
name, FastString
mod) ->
          if FastString -> Bool
isRattModule FastString
mod Bool -> Bool -> Bool
&& FastString
name forall a. Eq a => a -> a -> Bool
== FastString
"Stable"
          then forall (m :: * -> *) a. Monad m => a -> m a
return (Kind -> Maybe Var
getTyVar_maybe Kind
args)
          else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
        Maybe (FastString, FastString)
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing                           
    Maybe (TyCon, [Kind])
_ ->  forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing


data CheckExpr = CheckExpr{
  CheckExpr -> LCtx
recursiveSet :: Set Var,
  CheckExpr -> Expr Var
oldExpr :: Expr Var,
  CheckExpr -> Bool
fatalError :: Bool,
  CheckExpr -> Bool
verbose :: Bool,
  CheckExpr -> Bool
allowRecExp :: Bool
  }

checkExpr :: CheckExpr -> Expr Var -> CoreM ()
checkExpr :: CheckExpr -> Expr Var -> CoreM ()
checkExpr CheckExpr
c Expr Var
e = do
  Maybe TypeError
res <- Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (CheckExpr -> Ctx
emptyCtx CheckExpr
c) Expr Var
e
  case Maybe TypeError
res of
    Maybe TypeError
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just (TypeError SrcSpan
src SDoc
doc) ->
      let sev :: Severity
sev = if CheckExpr -> Bool
fatalError CheckExpr
c then Severity
SevError else Severity
SevWarning
      in if CheckExpr -> Bool
verbose CheckExpr
c then do
        forall (m :: * -> *).
(HasDynFlags m, MonadIO m, HasLogger m) =>
Severity -> SrcSpan -> SDoc -> m ()
printMessage Severity
sev SrcSpan
src (SDoc
"Internal error in Rattus Plugin: single tick transformation did not preserve typing." SDoc -> SDoc -> SDoc
$$ SDoc
doc)
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"-------- old --------"
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (SDoc -> String
showSDocUnsafe (forall a. Outputable a => a -> SDoc
ppr (CheckExpr -> Expr Var
oldExpr CheckExpr
c)))
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"-------- new --------"
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (SDoc -> String
showSDocUnsafe (forall a. Outputable a => a -> SDoc
ppr Expr Var
e))
         else
        forall (m :: * -> *).
(HasDynFlags m, MonadIO m, HasLogger m) =>
Severity -> SrcSpan -> SDoc -> m ()
printMessage Severity
sev SrcSpan
noSrcSpan (SDoc
"Internal error in Rattus Plugin: single tick transformation did not preserve typing." SDoc -> SDoc -> SDoc
$$
                             SDoc
"Compile with flags \"-fplugin-opt Rattus.Plugin:debug\" and \"-g2\" for detailed information")

checkExpr' :: Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' :: Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c (App Expr Var
e Expr Var
e') | forall {b}. Expr b -> Bool
isType Expr Var
e' Bool -> Bool -> Bool
|| (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Kind -> Bool
tcIsLiftedTypeKind forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Kind -> Kind
typeKind forall a b. (a -> b) -> a -> b
$ Expr Var -> Kind
exprType Expr Var
e')
  = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e
checkExpr' c :: Ctx
c@Ctx{current :: Ctx -> LCtx
current = LCtx
cur, hidden :: Ctx -> Hidden
hidden = Hidden
hid, earlier :: Ctx -> Maybe LCtx
earlier = Maybe LCtx
earl} (App Expr Var
e1 Expr Var
e2) =
  case Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e1 of
    Just (Prim
p,Var
v) -> case Prim
p of
      Prim
Box -> do
        Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
BoxApp Ctx
c) Expr Var
e2
      Prim
Arr -> do
        Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (HiddenReason -> Ctx -> Ctx
stabilize HiddenReason
BoxApp Ctx
c) Expr Var
e2

      Prim
Delay -> case Maybe LCtx
earl of
        Just LCtx
earl' ->
          Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{current :: LCtx
current = forall a. Set a
Set.empty, earlier :: Maybe LCtx
earlier = forall a. a -> Maybe a
Just LCtx
cur,
                      ticks :: Int
ticks = Ctx -> Int
ticks Ctx
c forall a. Num a => a -> a -> a
+ Int
1, hidden :: Hidden
hidden = Ctx -> Hidden
hidden Ctx
c forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const HiddenReason
DelayApp) LCtx
earl'} Expr Var
e2
        Maybe LCtx
Nothing -> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{current :: LCtx
current = forall a. Set a
Set.empty, earlier :: Maybe LCtx
earlier = forall a. a -> Maybe a
Just LCtx
cur, ticks :: Int
ticks = Ctx -> Int
ticks Ctx
c forall a. Num a => a -> a -> a
+ Int
1} Expr Var
e2
      Prim
Adv -> case Maybe LCtx
earl of
        Just LCtx
er -> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{earlier :: Maybe LCtx
earlier = forall a. Maybe a
Nothing, current :: LCtx
current = LCtx
er, ticks :: Int
ticks = Ctx -> Int
ticks Ctx
c forall a. Num a => a -> a -> a
- Int
1,
                               hidden :: Hidden
hidden = Hidden
hid forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const HiddenReason
AdvApp) LCtx
cur} Expr Var
e2
        Maybe LCtx
Nothing -> Ctx -> Var -> SDoc -> CoreM (Maybe TypeError)
typeError Ctx
c Var
v (String -> SDoc
text String
"can only advance under delay")
    Maybe (Prim, Var)
_ -> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e1)  (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e2)
checkExpr' Ctx
c (Case Expr Var
e Var
v Kind
_ [Alt Var]
alts) =
    forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e) (forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall a. Maybe a
Nothing)
                                   (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((\ (AltCon
_,[Var]
vs,Expr Var
e)-> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var]
vs Ctx
c') Expr Var
e) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {b}. Alt b -> (AltCon, [b], Expr b)
getAlt) [Alt Var]
alts))
  where c' :: Ctx
c' = [Var] -> Ctx -> Ctx
addVars [Var
v] Ctx
c
checkExpr' Ctx
c (Lam Var
v Expr Var
e)
  | Var -> Bool
isTyVar Var
v Bool -> Bool -> Bool
|| (Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ Kind -> Bool
tcIsLiftedTypeKind forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Kind -> Kind
typeKind forall a b. (a -> b) -> a -> b
$ Var -> Kind
varType Var
v) = do
      Maybe Var
is <- Kind -> CoreM (Maybe Var)
isStableConstr (Var -> Kind
varType Var
v)
      let c' :: Ctx
c' = case Maybe Var
is of
            Maybe Var
Nothing -> Ctx
c
            Just Var
t -> Ctx
c{stableTypes :: LCtx
stableTypes = forall a. Ord a => a -> Set a -> Set a
Set.insert Var
t (Ctx -> LCtx
stableTypes Ctx
c)}
      Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c' Expr Var
e
  | Bool
otherwise = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var
v] (Ctx -> Ctx
stabilizeLater Ctx
c)) Expr Var
e
checkExpr' Ctx
_ (Type Kind
_)  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
checkExpr' Ctx
_ (Lit Literal
_)  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
checkExpr' Ctx
_ (Coercion Coercion
_)  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
checkExpr' Ctx
c (Tick (SourceNote RealSrcSpan
span String
_name) Expr Var
e) =
  Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c{srcLoc :: SrcSpan
srcLoc = RealSrcSpan -> SrcSpan
fromRealSrcSpan RealSrcSpan
span} Expr Var
e
checkExpr' Ctx
c (Tick CoreTickish
_ Expr Var
e) = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e
checkExpr' Ctx
c (Cast Expr Var
e Coercion
_) = Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e
checkExpr' Ctx
c (Let (NonRec Var
v Expr Var
e1) Expr Var
e2) =
  case Ctx -> Expr Var -> Maybe (Prim, Var)
isPrimExpr Ctx
c Expr Var
e1 of
    Just (Prim
p,Var
_) -> (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (Ctx
c{primAlias :: Map Var Prim
primAlias = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Var
v Prim
p (Ctx -> Map Var Prim
primAlias Ctx
c)}) Expr Var
e2)
    Maybe (Prim, Var)
Nothing -> forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' Ctx
c Expr Var
e1)  (Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var
v] Ctx
c) Expr Var
e2)
checkExpr' Ctx
_ (Let (Rec ([])) Expr Var
_) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
checkExpr' Ctx
c (Let (Rec [(Var, Expr Var)]
binds) Expr Var
e2) = do
    [Maybe TypeError]
r1 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ (Var
v,Expr Var
e) -> Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' (Var -> Ctx
c' Var
v) Expr Var
e) [(Var, Expr Var)]
binds
    Maybe TypeError
r2 <- Ctx -> Expr Var -> CoreM (Maybe TypeError)
checkExpr' ([Var] -> Ctx -> Ctx
addVars [Var]
vs Ctx
c) Expr Var
e2
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall a. Maybe a
Nothing [Maybe TypeError]
r1 forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Maybe TypeError
r2)  
  where vs :: [Var]
vs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Var, Expr Var)]
binds
        ctxHid :: LCtx
ctxHid = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ctx -> LCtx
current Ctx
c) (forall a. Ord a => Set a -> Set a -> Set a
Set.union (Ctx -> LCtx
current Ctx
c)) (Ctx -> Maybe LCtx
earlier Ctx
c)
        c' :: Var -> Ctx
c' Var
v = Ctx
c {current :: LCtx
current = forall a. Set a
Set.empty,
                  earlier :: Maybe LCtx
earlier = forall a. Maybe a
Nothing,
                  hidden :: Hidden
hidden =  Ctx -> Hidden
hidden Ctx
c forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union`
                   (forall k a. (k -> a) -> Set k -> Map k a
Map.fromSet (forall a b. a -> b -> a
const (Var -> HiddenReason
NestedRec Var
v)) LCtx
ctxHid),
                  recDef :: LCtx
recDef = Ctx -> LCtx
recDef Ctx
c forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall a. Ord a => [a] -> Set a
Set.fromList [Var]
vs }
checkExpr' Ctx
c  (Var Var
v)
  | Kind -> Bool
tcIsLiftedTypeKind forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Kind -> Kind
typeKind forall a b. (a -> b) -> a -> b
$ Var -> Kind
varType Var
v =  case Ctx -> Var -> Scope
getScope Ctx
c Var
v of
             Hidden SDoc
reason -> Ctx -> Var -> SDoc -> CoreM (Maybe TypeError)
typeError Ctx
c Var
v SDoc
reason
             Scope
Visible -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  | Bool
otherwise = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing



addVars :: [Var] -> Ctx -> Ctx
addVars :: [Var] -> Ctx -> Ctx
addVars [Var]
v Ctx
c = Ctx
c{current :: LCtx
current = forall a. Ord a => [a] -> Set a
Set.fromList [Var]
v forall a. Ord a => Set a -> Set a -> Set a
`Set.union` Ctx -> LCtx
current Ctx
c }