{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE FlexibleInstances         #-}

{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- TODO(#1918): Only needed for GHC <9.0.1.

module Language.Haskell.Liquid.GHC.Play where

import Prelude hiding (error)

import           Control.Arrow       ((***))
import qualified Data.HashMap.Strict as M
import qualified Data.List           as L
import qualified Data.Maybe          as Mb

import Liquid.GHC.API as Ghc hiding (panic, showPpr)
import Language.Haskell.Liquid.GHC.Misc ()
import Language.Haskell.Liquid.Types.Errors
import Language.Haskell.Liquid.Types.Variance

-------------------------------------------------------------------------------
-- | Positivity Checker -------------------------------------------------------
-------------------------------------------------------------------------------

-- If the type constructor T is in the input list and its data constructors Di, Dj
-- use T in non strictly positive positions, 
-- then (T,(Di, Dj)) will appear in the result list.  

getNonPositivesTyCon :: [TyCon] -> [(TyCon, [DataCon])]
getNonPositivesTyCon :: [TyCon] -> [(TyCon, [DataCon])]
getNonPositivesTyCon [TyCon]
tcs = forall a b. (a -> Maybe b) -> [a] -> [b]
Mb.mapMaybe forall {b}. (TyCon, [(b, TyConOccurrence)]) -> Maybe (TyCon, [b])
go (forall k v. HashMap k v -> [(k, v)]
M.toList forall a b. (a -> b) -> a -> b
$ [TyCon] -> OccurrenceMap
makeOccurrences [TyCon]
tcs)
  where
    go :: (TyCon, [(b, TyConOccurrence)]) -> Maybe (TyCon, [b])
go (TyCon
tc,[(b, TyConOccurrence)]
dcocs) = case forall a. (a -> Bool) -> [a] -> [a]
filter (\(b
_,TyConOccurrence
occ) -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem TyCon
tc (TyConOccurrence -> [TyCon]
negOcc TyConOccurrence
occ)) [(b, TyConOccurrence)]
dcocs of
                      [] -> forall a. Maybe a
Nothing
                      [(b, TyConOccurrence)]
xs -> forall a. a -> Maybe a
Just (TyCon
tc, forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(b, TyConOccurrence)]
xs)


-- OccurrenceMap maps type constructors to their TyConOccurrence. 
-- for each of their data constructor. For example, for the below data definition
-- data T a = P (T a) | N (T a -> Int) | Both (T a -> T a) | None 
-- the entry below should get generated
--  OccurrenceMap 
-- = T |-> [(P, [
--          (P,    TyConOcc [T] [])
--          (N,    TyConOcc [Int] [T])
--          (Both, TyConOcc [T] [T])
--          (None, TyConOcc [] [])
--         ])] 
-- For positivity check, ultimately we only care about self occurences, 
-- but we keep track of all the TyCons for the mutually inductive data types. 
-- We separate the occurences per data constructor only to provide better error messages. 
type OccurrenceMap = M.HashMap TyCon [(DataCon, TyConOccurrence)]

data TyConOccurrence
    = TyConOcc { TyConOccurrence -> [TyCon]
posOcc :: [TyCon] -- TyCons that occur in positive positions
               , TyConOccurrence -> [TyCon]
negOcc :: [TyCon] -- TyCons that occur in negative positions
               }
  deriving TyConOccurrence -> TyConOccurrence -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TyConOccurrence -> TyConOccurrence -> Bool
$c/= :: TyConOccurrence -> TyConOccurrence -> Bool
== :: TyConOccurrence -> TyConOccurrence -> Bool
$c== :: TyConOccurrence -> TyConOccurrence -> Bool
Eq

instance Monoid TyConOccurrence where
  mempty :: TyConOccurrence
mempty = [TyCon] -> [TyCon] -> TyConOccurrence
TyConOcc forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
instance Semigroup TyConOccurrence where
  TyConOcc [TyCon]
p1 [TyCon]
n1 <> :: TyConOccurrence -> TyConOccurrence -> TyConOccurrence
<> TyConOcc [TyCon]
p2 [TyCon]
n2 = [TyCon] -> [TyCon] -> TyConOccurrence
TyConOcc (forall a. Eq a => [a] -> [a]
L.nub ([TyCon]
p1 forall a. Semigroup a => a -> a -> a
<> [TyCon]
p2)) (forall a. Eq a => [a] -> [a]
L.nub ([TyCon]
n1 forall a. Semigroup a => a -> a -> a
<> [TyCon]
n2))
instance Outputable TyConOccurrence where
  ppr :: TyConOccurrence -> SDoc
ppr (TyConOcc [TyCon]
pos [TyCon]
neg) = String -> SDoc
text String
"pos" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [TyCon]
pos SDoc -> SDoc -> SDoc
<+>  String -> SDoc
text String
"neg" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr [TyCon]
neg


instance Outputable OccurrenceMap where
  ppr :: OccurrenceMap -> SDoc
ppr OccurrenceMap
m = forall a. Outputable a => a -> SDoc
ppr (forall k v. HashMap k v -> [(k, v)]
M.toList OccurrenceMap
m)


makeOccurrences :: [TyCon] -> OccurrenceMap
makeOccurrences :: [TyCon] -> OccurrenceMap
makeOccurrences [TyCon]
tycons
  = let m0 :: OccurrenceMap
m0 = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList [(TyCon
tc, forall a b. (a -> b) -> [a] -> [b]
map (\DataCon
dc -> (DataCon
dc, HashMap TyCon VarianceInfo -> [Type] -> TyConOccurrence
makeOccurrence HashMap TyCon VarianceInfo
tcInfo (DataCon -> [Type]
dctypes DataCon
dc))) (TyCon -> [DataCon]
tyConDataCons TyCon
tc))
                        | TyCon
tc <- [TyCon]
tycons']
    -- fixpoint to find occurrences of mutually recursive data definitons
    in forall {t}. Eq t => (t -> t) -> t -> t
fix (\OccurrenceMap
m -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl OccurrenceMap -> TyCon -> OccurrenceMap
merge OccurrenceMap
m [TyCon]
tycons') OccurrenceMap
m0
  where
    fix :: (t -> t) -> t -> t
fix t -> t
f t
x = let x' :: t
x' = t -> t
f t
x in if t
x forall a. Eq a => a -> a -> Bool
== t
x' then t
x else (t -> t) -> t -> t
fix t -> t
f t
x'
    tcInfo :: HashMap TyCon VarianceInfo
tcInfo = forall k v. (Eq k, Hashable k) => [(k, v)] -> HashMap k v
M.fromList forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip [TyCon]
tycons' (TyCon -> VarianceInfo
makeTyConVariance forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyCon]
tycons')
    merge :: OccurrenceMap -> TyCon -> OccurrenceMap
merge OccurrenceMap
m TyCon
tc = forall k a.
(Eq k, Hashable k) =>
(a -> Maybe a) -> k -> HashMap k a -> HashMap k a
M.update (forall {a}.
OccurrenceMap
-> [(a, TyConOccurrence)] -> Maybe [(a, TyConOccurrence)]
mergeList OccurrenceMap
m) TyCon
tc OccurrenceMap
m
    mergeList :: OccurrenceMap
-> [(a, TyConOccurrence)] -> Maybe [(a, TyConOccurrence)]
mergeList OccurrenceMap
m [(a, TyConOccurrence)]
xs = forall a. a -> Maybe a
Just [(a
dc, OccurrenceMap -> TyConOccurrence -> TyConOccurrence
mergeApp OccurrenceMap
m TyConOccurrence
am) | (a
dc,TyConOccurrence
am) <- [(a, TyConOccurrence)]
xs]
    mergeApp :: OccurrenceMap -> TyConOccurrence -> TyConOccurrence
mergeApp OccurrenceMap
m (TyConOcc [TyCon]
pos [TyCon]
neg) =
        let TyConOcc [TyCon]
pospos [TyCon]
posneg = forall a. Monoid a => [a] -> a
mconcat (OccurrenceMap -> TyCon -> TyConOccurrence
findOccurrence OccurrenceMap
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyCon]
pos)
            TyConOcc [TyCon]
negpos [TyCon]
negneg = forall a. Monoid a => [a] -> a
mconcat (OccurrenceMap -> TyCon -> TyConOccurrence
findOccurrence OccurrenceMap
m forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TyCon]
neg)
        -- Keep positive, flip negative 
        in [TyCon] -> [TyCon] -> TyConOccurrence
TyConOcc (forall a. Eq a => [a] -> [a]
L.nub ([TyCon]
pos forall a. Semigroup a => a -> a -> a
<> [TyCon]
pospos forall a. Semigroup a => a -> a -> a
<> [TyCon]
negneg)) (forall a. Eq a => [a] -> [a]
L.nub ([TyCon]
neg forall a. Semigroup a => a -> a -> a
<> [TyCon]
negpos forall a. Semigroup a => a -> a -> a
<> [TyCon]
posneg))


    tycontypes :: TyCon -> [Type]
tycontypes TyCon
tc = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap DataCon -> [Type]
dctypes forall a b. (a -> b) -> a -> b
$ TyCon -> [DataCon]
tyConDataCons TyCon
tc
    dctypes :: DataCon -> [Type]
dctypes    DataCon
dc = forall a. Scaled a -> a
irrelevantMult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> DataCon -> [Scaled Type]
dataConOrigArgTys DataCon
dc

    -- Construct the map for all TyCons that appear in the definitions 
    tycons' :: [TyCon]
tycons' = forall a. Eq a => [a] -> [a]
L.nub (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TyCon]
tcs (forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap TyCon -> [Type]
tycontypes [TyCon]
tycons) forall a. [a] -> [a] -> [a]
++ [TyCon]
tycons)

    tcs :: Type -> [TyCon]
tcs (TyConApp TyCon
tc' [Type]
ts) = TyCon
tc'forall a. a -> [a] -> [a]
: forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Type -> [TyCon]
tcs [Type]
ts
    tcs (AppTy Type
t1 Type
t2)     = Type -> [TyCon]
tcs Type
t1 forall a. [a] -> [a] -> [a]
++ Type -> [TyCon]
tcs Type
t2
    tcs (ForAllTy TyCoVarBinder
_ Type
t)    = Type -> [TyCon]
tcs Type
t
    tcs (FunTy AnonArgFlag
_ Type
_ Type
t1 Type
t2) = Type -> [TyCon]
tcs Type
t1 forall a. [a] -> [a] -> [a]
++ Type -> [TyCon]
tcs Type
t2
    tcs (TyVarTy Var
_ )      = []
    tcs (LitTy TyLit
_)         = []
    tcs (CastTy Type
_ KindCoercion
_)      = []
    tcs (CoercionTy KindCoercion
_)    = []

makeOccurrence :: M.HashMap TyCon VarianceInfo -> [Type] -> TyConOccurrence
makeOccurrence :: HashMap TyCon VarianceInfo -> [Type] -> TyConOccurrence
makeOccurrence HashMap TyCon VarianceInfo
tcInfo = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Variance -> TyConOccurrence -> Type -> TyConOccurrence
go Variance
Covariant) forall a. Monoid a => a
mempty
  where
    go :: Variance -> TyConOccurrence -> Type -> TyConOccurrence
    go :: Variance -> TyConOccurrence -> Type -> TyConOccurrence
go Variance
p TyConOccurrence
m (TyConApp TyCon
tc [Type]
ts)  = Variance -> TyCon -> TyConOccurrence -> TyConOccurrence
addOccurrence Variance
p TyCon
tc
                             forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\TyConOccurrence
m' (Type
t, Variance
v) -> Variance -> TyConOccurrence -> Type -> TyConOccurrence
go (Variance
v forall a. Semigroup a => a -> a -> a
<> Variance
p) TyConOccurrence
m' Type
t) TyConOccurrence
m
                                (forall a b. [a] -> [b] -> [(a, b)]
zip [Type]
ts (forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (forall a. a -> [a]
repeat Variance
Bivariant) TyCon
tc HashMap TyCon VarianceInfo
tcInfo))
    go Variance
_ TyConOccurrence
m (TyVarTy Var
_ )      = TyConOccurrence
m
    go Variance
_ TyConOccurrence
m (AppTy Type
t1 Type
t2)     = Variance -> TyConOccurrence -> Type -> TyConOccurrence
go Variance
Bivariant (Variance -> TyConOccurrence -> Type -> TyConOccurrence
go Variance
Bivariant TyConOccurrence
m Type
t1) Type
t2
    go Variance
p TyConOccurrence
m (ForAllTy TyCoVarBinder
_ Type
t)    = Variance -> TyConOccurrence -> Type -> TyConOccurrence
go Variance
p TyConOccurrence
m Type
t
    go Variance
p TyConOccurrence
m (FunTy AnonArgFlag
_ Type
_ Type
t1 Type
t2) = Variance -> TyConOccurrence -> Type -> TyConOccurrence
go Variance
p (Variance -> TyConOccurrence -> Type -> TyConOccurrence
go (Variance -> Variance
flipVariance Variance
p) TyConOccurrence
m Type
t1) Type
t2
    go Variance
_ TyConOccurrence
m (LitTy TyLit
_)         = TyConOccurrence
m
    go Variance
_ TyConOccurrence
m (CastTy Type
_ KindCoercion
_)      = TyConOccurrence
m
    go Variance
_ TyConOccurrence
m (CoercionTy KindCoercion
_)    = TyConOccurrence
m

    addOccurrence :: Variance -> TyCon -> TyConOccurrence -> TyConOccurrence
addOccurrence Variance
p TyCon
tc (TyConOcc [TyCon]
pos [TyCon]
neg)
      = case Variance
p of
         Variance
Covariant     -> [TyCon] -> [TyCon] -> TyConOccurrence
TyConOcc (forall a. Eq a => [a] -> [a]
L.nub (TyCon
tcforall a. a -> [a] -> [a]
:[TyCon]
pos)) [TyCon]
neg
         Variance
Contravariant -> [TyCon] -> [TyCon] -> TyConOccurrence
TyConOcc [TyCon]
pos (forall a. Eq a => [a] -> [a]
L.nub (TyCon
tcforall a. a -> [a] -> [a]
:[TyCon]
neg))
         Variance
Bivariant     -> [TyCon] -> [TyCon] -> TyConOccurrence
TyConOcc (forall a. Eq a => [a] -> [a]
L.nub (TyCon
tcforall a. a -> [a] -> [a]
:[TyCon]
pos)) (forall a. Eq a => [a] -> [a]
L.nub (TyCon
tcforall a. a -> [a] -> [a]
:[TyCon]
neg))
         Variance
Invariant     -> [TyCon] -> [TyCon] -> TyConOccurrence
TyConOcc [TyCon]
pos [TyCon]
neg

findOccurrence :: OccurrenceMap -> TyCon -> TyConOccurrence
findOccurrence :: OccurrenceMap -> TyCon -> TyConOccurrence
findOccurrence OccurrenceMap
m TyCon
tc = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault forall a. Monoid a => a
mempty TyCon
tc OccurrenceMap
m)




isRecursivenewTyCon :: TyCon -> Bool
isRecursivenewTyCon :: TyCon -> Bool
isRecursivenewTyCon TyCon
c
  | Bool -> Bool
not (TyCon -> Bool
isNewTyCon TyCon
c)
  = Bool
False
isRecursivenewTyCon TyCon
c
  = Type -> Bool
go Type
t
  where
    t :: Type
t = forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ TyCon -> ([Var], Type)
newTyConRhs TyCon
c
    go :: Type -> Bool
go (AppTy Type
t1 Type
t2)      = Type -> Bool
go Type
t1 Bool -> Bool -> Bool
|| Type -> Bool
go Type
t2
    go (TyConApp TyCon
c' [Type]
ts)   = TyCon
c forall a. Eq a => a -> a -> Bool
== TyCon
c' Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Type -> Bool
go [Type]
ts
    go (ForAllTy TyCoVarBinder
_ Type
t1)    = Type -> Bool
go Type
t1
    go (FunTy AnonArgFlag
_ Type
_ Type
t1 Type
t2)  = Type -> Bool
go Type
t1 Bool -> Bool -> Bool
|| Type -> Bool
go Type
t2
    go (CastTy Type
t1 KindCoercion
_)      = Type -> Bool
go Type
t1
    go Type
_                  = Bool
False


dataConImplicitIds :: DataCon -> [Id]
dataConImplicitIds :: DataCon -> [Var]
dataConImplicitIds DataCon
dc = [ Var
x | AnId Var
x <- DataCon -> [TyThing]
dataConImplicitTyThings DataCon
dc]

class Subable a where
  sub   :: M.HashMap CoreBndr CoreExpr -> a -> a
  subTy :: M.HashMap TyVar Type -> a -> a

instance Subable CoreExpr where
  sub :: HashMap Var CoreExpr -> CoreExpr -> CoreExpr
sub HashMap Var CoreExpr
s (Var Var
v)        = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault (forall b. Var -> Expr b
Var Var
v) Var
v HashMap Var CoreExpr
s
  sub HashMap Var CoreExpr
_ (Lit Literal
l)        = forall b. Literal -> Expr b
Lit Literal
l
  sub HashMap Var CoreExpr
s (App CoreExpr
e1 CoreExpr
e2)    = forall b. Expr b -> Expr b -> Expr b
App (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e1) (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e2)
  sub HashMap Var CoreExpr
s (Lam Var
b CoreExpr
e)      = forall b. b -> Expr b -> Expr b
Lam Var
b (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e)
  sub HashMap Var CoreExpr
s (Let Bind Var
b CoreExpr
e)      = forall b. Bind b -> Expr b -> Expr b
Let (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s Bind Var
b) (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e)
  sub HashMap Var CoreExpr
s (Case CoreExpr
e Var
b Type
t [Alt Var]
a) = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e) (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s Var
b) Type
t (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s) [Alt Var]
a)
  sub HashMap Var CoreExpr
s (Cast CoreExpr
e KindCoercion
c)     = forall b. Expr b -> KindCoercion -> Expr b
Cast (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e) KindCoercion
c
  sub HashMap Var CoreExpr
s (Tick CoreTickish
t CoreExpr
e)     = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e)
  sub HashMap Var CoreExpr
_ (Type Type
t)       = forall b. Type -> Expr b
Type Type
t
  sub HashMap Var CoreExpr
_ (Coercion KindCoercion
c)   = forall b. KindCoercion -> Expr b
Coercion KindCoercion
c

  subTy :: HashMap Var Type -> CoreExpr -> CoreExpr
subTy HashMap Var Type
s (Var Var
v)      = forall b. Var -> Expr b
Var (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s Var
v)
  subTy HashMap Var Type
_ (Lit Literal
l)      = forall b. Literal -> Expr b
Lit Literal
l
  subTy HashMap Var Type
s (App CoreExpr
e1 CoreExpr
e2)  = forall b. Expr b -> Expr b -> Expr b
App (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e1) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e2)
  subTy HashMap Var Type
s (Lam Var
b CoreExpr
e)    | Var -> Bool
isTyVar Var
b = forall b. b -> Expr b -> Expr b
Lam Var
v' (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e)
   where v' :: Var
v' = case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup Var
b HashMap Var Type
s of
               Just (TyVarTy Var
v) -> Var
v
               Maybe Type
_                -> Var
b

  subTy HashMap Var Type
s (Lam Var
b CoreExpr
e)      = forall b. b -> Expr b -> Expr b
Lam (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s Var
b) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e)
  subTy HashMap Var Type
s (Let Bind Var
b CoreExpr
e)      = forall b. Bind b -> Expr b -> Expr b
Let (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s Bind Var
b) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e)
  subTy HashMap Var Type
s (Case CoreExpr
e Var
b Type
t [Alt Var]
a) = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s Var
b) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s Type
t) (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s) [Alt Var]
a)
  subTy HashMap Var Type
s (Cast CoreExpr
e KindCoercion
c)     = forall b. Expr b -> KindCoercion -> Expr b
Cast (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s KindCoercion
c)
  subTy HashMap Var Type
s (Tick CoreTickish
t CoreExpr
e)     = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e)
  subTy HashMap Var Type
s (Type Type
t)       = forall b. Type -> Expr b
Type (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s Type
t)
  subTy HashMap Var Type
s (Coercion KindCoercion
c)   = forall b. KindCoercion -> Expr b
Coercion (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s KindCoercion
c)

instance Subable Coercion where
  sub :: HashMap Var CoreExpr -> KindCoercion -> KindCoercion
sub HashMap Var CoreExpr
_ KindCoercion
c                = KindCoercion
c
  subTy :: HashMap Var Type -> KindCoercion -> KindCoercion
subTy HashMap Var Type
_ KindCoercion
_              = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"subTy Coercion"

instance Subable (Alt Var) where
 sub :: HashMap Var CoreExpr -> Alt Var -> Alt Var
sub HashMap Var CoreExpr
s (Alt AltCon
a [Var]
b CoreExpr
e)   = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
a (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s) [Var]
b)   (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e)
 subTy :: HashMap Var Type -> Alt Var -> Alt Var
subTy HashMap Var Type
s (Alt AltCon
a [Var]
b CoreExpr
e) = forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
a (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s) [Var]
b) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e)

instance Subable Var where
 sub :: HashMap Var CoreExpr -> Var -> Var
sub HashMap Var CoreExpr
s Var
v   | forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member Var
v HashMap Var CoreExpr
s = forall t. Expr t -> Var
subVar forall a b. (a -> b) -> a -> b
$ HashMap Var CoreExpr
s forall k v.
(Eq k, Hashable k, HasCallStack) =>
HashMap k v -> k -> v
M.! Var
v
           | Bool
otherwise    = Var
v
 subTy :: HashMap Var Type -> Var -> Var
subTy HashMap Var Type
s Var
v = Var -> Type -> Var
setVarType Var
v (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s (Var -> Type
varType Var
v))

subVar :: Expr t -> Id
subVar :: forall t. Expr t -> Var
subVar (Var Var
x) = Var
x
subVar  Expr t
_      = forall a. Maybe SrcSpan -> String -> a
panic forall a. Maybe a
Nothing String
"sub Var"

instance Subable (Bind Var) where
 sub :: HashMap Var CoreExpr -> Bind Var -> Bind Var
sub HashMap Var CoreExpr
s (NonRec Var
x CoreExpr
e)   = forall b. b -> Expr b -> Bind b
NonRec (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s Var
x) (forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s CoreExpr
e)
 sub HashMap Var CoreExpr
s (Rec [(Var, CoreExpr)]
xes)      = forall b. [(b, Expr b)] -> Bind b
Rec ((forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. Subable a => HashMap Var CoreExpr -> a -> a
sub HashMap Var CoreExpr
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)

 subTy :: HashMap Var Type -> Bind Var -> Bind Var
subTy HashMap Var Type
s (NonRec Var
x CoreExpr
e) = forall b. b -> Expr b -> Bind b
NonRec (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s Var
x) (forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s CoreExpr
e)
 subTy HashMap Var Type
s (Rec [(Var, CoreExpr)]
xes)    = forall b. [(b, Expr b)] -> Bind b
Rec ((forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s  forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall a. Subable a => HashMap Var Type -> a -> a
subTy HashMap Var Type
s) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Var, CoreExpr)]
xes)

instance Subable Type where
 sub :: HashMap Var CoreExpr -> Type -> Type
sub HashMap Var CoreExpr
_ Type
e   = Type
e
 subTy :: HashMap Var Type -> Type -> Type
subTy     = HashMap Var Type -> Type -> Type
substTysWith

substTysWith :: M.HashMap Var Type -> Type -> Type
substTysWith :: HashMap Var Type -> Type -> Type
substTysWith HashMap Var Type
s tv :: Type
tv@(TyVarTy Var
v)      = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Type
tv Var
v HashMap Var Type
s
substTysWith HashMap Var Type
s (FunTy AnonArgFlag
aaf Type
m Type
t1 Type
t2) = AnonArgFlag -> Type -> Type -> Type -> Type
FunTy AnonArgFlag
aaf Type
m (HashMap Var Type -> Type -> Type
substTysWith HashMap Var Type
s Type
t1) (HashMap Var Type -> Type -> Type
substTysWith HashMap Var Type
s Type
t2)
substTysWith HashMap Var Type
s (ForAllTy TyCoVarBinder
v Type
t)      = TyCoVarBinder -> Type -> Type
ForAllTy TyCoVarBinder
v (HashMap Var Type -> Type -> Type
substTysWith (forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (forall tv argf. VarBndr tv argf -> tv
binderVar TyCoVarBinder
v) HashMap Var Type
s) Type
t)
substTysWith HashMap Var Type
s (TyConApp TyCon
c [Type]
ts)     = TyCon -> [Type] -> Type
TyConApp TyCon
c (forall a b. (a -> b) -> [a] -> [b]
map (HashMap Var Type -> Type -> Type
substTysWith HashMap Var Type
s) [Type]
ts)
substTysWith HashMap Var Type
s (AppTy Type
t1 Type
t2)       = Type -> Type -> Type
AppTy (HashMap Var Type -> Type -> Type
substTysWith HashMap Var Type
s Type
t1) (HashMap Var Type -> Type -> Type
substTysWith HashMap Var Type
s Type
t2)
substTysWith HashMap Var Type
_ (LitTy TyLit
t)           = TyLit -> Type
LitTy TyLit
t
substTysWith HashMap Var Type
s (CastTy Type
t KindCoercion
c)        = Type -> KindCoercion -> Type
CastTy (HashMap Var Type -> Type -> Type
substTysWith HashMap Var Type
s Type
t) KindCoercion
c
substTysWith HashMap Var Type
_ (CoercionTy KindCoercion
c)      = KindCoercion -> Type
CoercionTy KindCoercion
c

substExpr :: M.HashMap Var Var -> CoreExpr -> CoreExpr
substExpr :: HashMap Var Var -> CoreExpr -> CoreExpr
substExpr HashMap Var Var
s = CoreExpr -> CoreExpr
go
  where
    subsVar :: Var -> Var
subsVar Var
v                = forall k v. (Eq k, Hashable k) => v -> k -> HashMap k v -> v
M.lookupDefault Var
v Var
v HashMap Var Var
s
    go :: CoreExpr -> CoreExpr
go (Var Var
v)               = forall b. Var -> Expr b
Var forall a b. (a -> b) -> a -> b
$ Var -> Var
subsVar Var
v
    go (Lit Literal
l)               = forall b. Literal -> Expr b
Lit Literal
l
    go (App CoreExpr
e1 CoreExpr
e2)           = forall b. Expr b -> Expr b -> Expr b
App (CoreExpr -> CoreExpr
go CoreExpr
e1) (CoreExpr -> CoreExpr
go CoreExpr
e2)
    go (Lam Var
x CoreExpr
e)             = forall b. b -> Expr b -> Expr b
Lam (Var -> Var
subsVar Var
x) (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Let (NonRec Var
x CoreExpr
ex) CoreExpr
e) = forall b. Bind b -> Expr b -> Expr b
Let (forall b. b -> Expr b -> Bind b
NonRec (Var -> Var
subsVar Var
x) (CoreExpr -> CoreExpr
go CoreExpr
ex)) (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Let (Rec [(Var, CoreExpr)]
xes) CoreExpr
e)     = forall b. Bind b -> Expr b -> Expr b
Let (forall b. [(b, Expr b)] -> Bind b
Rec [(Var -> Var
subsVar Var
x', CoreExpr -> CoreExpr
go CoreExpr
e') | (Var
x',CoreExpr
e') <- [(Var, CoreExpr)]
xes]) (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Case CoreExpr
e Var
b Type
t [Alt Var]
alts)     = forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case (CoreExpr -> CoreExpr
go CoreExpr
e) (Var -> Var
subsVar Var
b) Type
t [forall b. AltCon -> [b] -> Expr b -> Alt b
Alt AltCon
c (Var -> Var
subsVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Var]
xs) (CoreExpr -> CoreExpr
go CoreExpr
e') | Alt AltCon
c [Var]
xs CoreExpr
e' <- [Alt Var]
alts]
    go (Cast CoreExpr
e KindCoercion
c)            = forall b. Expr b -> KindCoercion -> Expr b
Cast (CoreExpr -> CoreExpr
go CoreExpr
e) KindCoercion
c
    go (Tick CoreTickish
t CoreExpr
e)            = forall b. CoreTickish -> Expr b -> Expr b
Tick CoreTickish
t (CoreExpr -> CoreExpr
go CoreExpr
e)
    go (Type Type
t)              = forall b. Type -> Expr b
Type Type
t
    go (Coercion KindCoercion
c)          = forall b. KindCoercion -> Expr b
Coercion KindCoercion
c

mapType :: (Type -> Type) -> Type -> Type
mapType :: (Type -> Type) -> Type -> Type
mapType Type -> Type
f = Type -> Type
go
  where
    go :: Type -> Type
go t :: Type
t@(TyVarTy Var
_)        = Type -> Type
f Type
t
    go (AppTy Type
t1 Type
t2)        = Type -> Type
f forall a b. (a -> b) -> a -> b
$ Type -> Type -> Type
AppTy (Type -> Type
go Type
t1) (Type -> Type
go Type
t2)
    go (TyConApp TyCon
c [Type]
ts)      = Type -> Type
f forall a b. (a -> b) -> a -> b
$ TyCon -> [Type] -> Type
TyConApp TyCon
c (Type -> Type
go forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Type]
ts)
    go (FunTy AnonArgFlag
aaf Type
m Type
t1 Type
t2)  = Type -> Type
f forall a b. (a -> b) -> a -> b
$ AnonArgFlag -> Type -> Type -> Type -> Type
FunTy AnonArgFlag
aaf Type
m (Type -> Type
go Type
t1) (Type -> Type
go Type
t2)
    go (ForAllTy TyCoVarBinder
v Type
t)       = Type -> Type
f forall a b. (a -> b) -> a -> b
$ TyCoVarBinder -> Type -> Type
ForAllTy TyCoVarBinder
v (Type -> Type
go Type
t)
    go t :: Type
t@(LitTy TyLit
_)          = Type -> Type
f Type
t
    go (CastTy Type
t KindCoercion
c)         = Type -> KindCoercion -> Type
CastTy (Type -> Type
go Type
t) KindCoercion
c
    go (CoercionTy KindCoercion
c)       = Type -> Type
f forall a b. (a -> b) -> a -> b
$ KindCoercion -> Type
CoercionTy KindCoercion
c


stringClassArg :: Type -> Maybe Type
stringClassArg :: Type -> Maybe Type
stringClassArg Type
t | Type -> Bool
isFunTy Type
t
  = forall a. Maybe a
Nothing
stringClassArg Type
t
  = case (Type -> Maybe TyCon
tyConAppTyCon_maybe Type
t, Type -> Maybe [Type]
tyConAppArgs_maybe Type
t) of
      (Just TyCon
c, Just [Type
t']) | Name
isStringClassName forall a. Eq a => a -> a -> Bool
== TyCon -> Name
tyConName TyCon
c
           -> forall a. a -> Maybe a
Just Type
t'
      (Maybe TyCon, Maybe [Type])
_    -> forall a. Maybe a
Nothing