{-# LANGUAGE CPP #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
module Clash.Core.Util where
import Control.Concurrent.Supply (Supply, freshId)
import qualified Control.Lens as Lens
import Control.Monad.Trans.Except (Except, throwE)
import Data.Coerce (coerce)
import qualified Data.IntSet as IntSet
import qualified Data.HashSet as HashSet
import Data.List
(foldl', mapAccumR, elemIndices, nub)
import Data.Maybe (fromJust, mapMaybe, catMaybes)
import qualified Data.Text as T
import Data.Text.Prettyprint.Doc (line)
#if !MIN_VERSION_base(4,11,0)
import Data.Semigroup
#endif
import Clash.Core.DataCon
(DataCon (MkData), dcType, dcUnivTyVars, dcExtTyVars, dcArgTys)
import Clash.Core.FreeVars
(termFreeVarsX, tyFVsOfTypes, typeFreeVars)
import Clash.Core.Literal (literalType)
import Clash.Core.Name
(Name (..), OccName, mkUnsafeInternalName, mkUnsafeSystemName)
import Clash.Core.Pretty (ppr, showPpr)
import Clash.Core.Subst
(extendTvSubst, mkSubst, mkTvSubst, substTy, substTyWith,
substTyInVar, extendTvSubstList)
import Clash.Core.Term
(LetBinding, Pat (..), PrimInfo (..), Term (..), Alt, WorkInfo (..),
TickInfo (..), collectArgs)
import Clash.Core.Type
(Kind, LitTy (..), Type (..), TypeView (..),
coreView, coreView1, isFunTy, isPolyFunCoreTy, mkFunTy, splitFunTy, tyView,
undefinedTy, isTypeFamilyApplication)
import Clash.Core.TyCon
(TyConMap, tyConDataCons)
import Clash.Core.TysPrim (typeNatKind)
import Clash.Core.Var
(Id, TyVar, Var (..), isLocalId, mkLocalId, mkTyVar)
import Clash.Core.VarEnv
(InScopeSet, VarEnv, emptyVarEnv, extendInScopeSet, extendVarEnv,
lookupVarEnv, mkInScopeSet, uniqAway, extendInScopeSetList, unionInScope,
mkVarSet, unionVarSet, unitVarSet, emptyVarSet)
import Clash.Unique
import Clash.Util
type Gamma = VarEnv Type
type Delta = VarEnv Kind
normalizeAdd
:: (Type, Type)
-> Maybe (Integer, Integer, Type)
normalizeAdd (a, b) = do
(n, rhs) <- lhsLit a b
case tyView rhs of
TyConApp (nameOcc -> "GHC.TypeNats.+") [left, right] -> do
(m, o) <- lhsLit left right
return (n, m, o)
_ ->
Nothing
where
lhsLit x (LitTy (NumTy n)) = Just (n, x)
lhsLit (LitTy (NumTy n)) y = Just (n, y)
lhsLit _ _ = Nothing
data TypeEqSolution
= Solution (TyVar, Type)
| AbsurdSolution
| NoSolution
deriving (Show, Eq)
catSolutions :: [TypeEqSolution] -> [(TyVar, Type)]
catSolutions = mapMaybe getSol
where
getSol (Solution s) = Just s
getSol _ = Nothing
solveNonAbsurds :: TyConMap -> [(Type, Type)] -> [(TyVar, Type)]
solveNonAbsurds _tcm [] = []
solveNonAbsurds tcm (eq:eqs) =
solved ++ solveNonAbsurds tcm eqs
where
solvers = [pure . solveAdd, solveEq tcm]
solved = catSolutions (concat [s eq | s <- solvers])
solveEq :: TyConMap -> (Type, Type) -> [TypeEqSolution]
solveEq tcm (coreView tcm -> left, coreView tcm -> right) =
case (left, right) of
(VarTy tyVar, ConstTy {}) ->
[Solution (tyVar, right)]
(ConstTy {}, VarTy tyVar) ->
[Solution (tyVar, left)]
(ConstTy {}, ConstTy {}) ->
if left /= right then [AbsurdSolution] else []
(LitTy {}, LitTy {}) ->
if left /= right then [AbsurdSolution] else []
_ ->
if any (isTypeFamilyApplication tcm) [left, right] then
[]
else
case (tyView left, tyView right) of
(TyConApp leftNm leftTys, TyConApp rightNm rightTys) ->
if leftNm == rightNm then
concat (map (solveEq tcm) (zip leftTys rightTys))
else
[AbsurdSolution]
_ ->
[]
solveAdd
:: (Type, Type)
-> TypeEqSolution
solveAdd ab =
case normalizeAdd ab of
Just (n, m, VarTy tyVar) ->
if n >= 0 && m >= 0 && n - m >= 0 then
Solution (tyVar, (LitTy (NumTy (n - m))))
else
AbsurdSolution
_ ->
NoSolution
typeEq
:: TyConMap
-> Type
-> Maybe (Type, Type)
typeEq tcm ty =
case tyView (coreView tcm ty) of
TyConApp (nameOcc -> "GHC.Prim.~#") [_, _, left, right] ->
Just (coreView tcm left, coreView tcm right)
_ ->
Nothing
altEqs
:: TyConMap
-> Alt
-> [(Type, Type)]
altEqs tcm (pat, _term) =
catMaybes (map (typeEq tcm . varType) (snd (patIds pat)))
isAbsurdAlt
:: TyConMap
-> Alt
-> Bool
isAbsurdAlt tcm alt =
any (isAbsurdEq tcm) (altEqs tcm alt)
isAbsurdEq
:: TyConMap
-> (Type, Type)
-> Bool
isAbsurdEq tcm ((left0, right0)) =
case (coreView tcm left0, coreView tcm right0) of
(solveAdd -> AbsurdSolution) -> True
lr -> any (==AbsurdSolution) (solveEq tcm lr)
substGlobalsInExistentials
:: HasCallStack
=> InScopeSet
-> [TyVar]
-> [(TyVar, Type)]
-> [TyVar]
substGlobalsInExistentials is exts substs0 = result
where
iss = scanl extendInScopeSet is exts
substs1 = map (\is_ -> extendTvSubstList (mkSubst is_) substs0) iss
result = zipWith substTyInVar substs1 exts
substInExistentialsList
:: HasCallStack
=> InScopeSet
-> [TyVar]
-> [(TyVar, Type)]
-> [TyVar]
substInExistentialsList is exts substs =
foldl (substInExistentials is) exts substs
substInExistentials
:: HasCallStack
=> InScopeSet
-> [TyVar]
-> (TyVar, Type)
-> [TyVar]
substInExistentials is exts subst@(typeVar, _type) =
case elemIndices typeVar exts of
[] ->
substGlobalsInExistentials is exts [subst]
(last -> i) ->
take (i+1) exts ++ substGlobalsInExistentials is (drop (i+1) exts) [subst]
termType
:: TyConMap
-> Term
-> Type
termType m e = case e of
Var t -> varType t
Data dc -> dcType dc
Literal l -> literalType l
Prim _ t -> primType t
Lam v e' -> mkFunTy (varType v) (termType m e')
TyLam tv e' -> ForAllTy tv (termType m e')
App _ _ -> case collectArgs e of
(fun, args) -> applyTypeToArgs e m (termType m fun) args
TyApp _ _ -> case collectArgs e of
(fun, args) -> applyTypeToArgs e m (termType m fun) args
Letrec _ e' -> termType m e'
Case _ ty _ -> ty
Cast _ _ ty2 -> ty2
Tick _ e' -> termType m e'
collectBndrs :: Term
-> ([Either Id TyVar], Term)
collectBndrs = go []
where
go bs (Lam v e') = go (Left v:bs) e'
go bs (TyLam tv e') = go (Right tv:bs) e'
go bs e' = (reverse bs,e')
applyTypeToArgs
:: Term
-> TyConMap
-> Type
-> [Either Term Type]
-> Type
applyTypeToArgs e m opTy args = go opTy args
where
go opTy' [] = opTy'
go opTy' (Right ty:args') = goTyArgs opTy' [ty] args'
go opTy' (Left _:args') = case splitFunTy m opTy' of
Just (_,resTy) -> go resTy args'
_ -> error $ unlines ["applyTypeToArgs:"
,"Expression: " ++ showPpr e
,"Type: " ++ showPpr opTy
,"Args: " ++ unlines (map (either showPpr showPpr) args)
]
goTyArgs opTy' revTys (Right ty:args') = goTyArgs opTy' (ty:revTys) args'
goTyArgs opTy' revTys args' = go (piResultTys m opTy' (reverse revTys)) args'
piResultTy
:: TyConMap
-> Type
-> Type
-> Type
piResultTy m ty arg = case piResultTyMaybe m ty arg of
Just res -> res
Nothing -> pprPanic "piResultTy" (ppr ty <> line <> ppr arg)
piResultTyMaybe
:: TyConMap
-> Type
-> Type
-> Maybe Type
piResultTyMaybe m ty arg
| Just ty' <- coreView1 m ty
= piResultTyMaybe m ty' arg
| FunTy _ res <- tyView ty
= Just res
| ForAllTy tv res <- ty
= let emptySubst = mkSubst (mkInScopeSet (tyFVsOfTypes [arg,res]))
in Just (substTy (extendTvSubst emptySubst tv arg) res)
| otherwise
= Nothing
piResultTys
:: TyConMap
-> Type
-> [Type]
-> Type
piResultTys _ ty [] = ty
piResultTys m ty origArgs@(arg:args)
| Just ty' <- coreView1 m ty
= piResultTys m ty' origArgs
| FunTy _ res <- tyView ty
= piResultTys m res args
| ForAllTy tv res <- ty
= go (extendVarEnv tv arg emptyVarEnv) res args
| otherwise
= pprPanic "piResultTys1" (ppr ty <> line <> ppr origArgs)
where
inScope = mkInScopeSet (tyFVsOfTypes (ty:origArgs))
go env ty' [] = substTy (mkTvSubst inScope env) ty'
go env ty' allArgs@(arg':args')
| Just ty'' <- coreView1 m ty'
= go env ty'' allArgs
| FunTy _ res <- tyView ty'
= go env res args'
| ForAllTy tv res <- ty'
= go (extendVarEnv tv arg' env) res args'
| VarTy tv <- ty'
, Just ty'' <- lookupVarEnv tv env
= piResultTys m ty'' allArgs
| otherwise
= pprPanic "piResultTys2" (ppr ty' <> line <> ppr origArgs <> line <> ppr allArgs)
patIds :: Pat -> ([TyVar],[Id])
patIds (DataPat _ tvs ids) = (tvs,ids)
patIds _ = ([],[])
patVars :: Pat -> [Var a]
patVars (DataPat _ tvs ids) = coerce tvs ++ coerce ids
patVars _ = []
mkAbstraction :: Term
-> [Either Id TyVar]
-> Term
mkAbstraction = foldr (either Lam TyLam)
mkTyLams :: Term
-> [TyVar]
-> Term
mkTyLams tm = mkAbstraction tm . map Right
mkLams :: Term
-> [Id]
-> Term
mkLams tm = mkAbstraction tm . map Left
mkApps :: Term
-> [Either Term Type]
-> Term
mkApps = foldl' (\e a -> either (App e) (TyApp e) a)
mkTmApps :: Term
-> [Term]
-> Term
mkTmApps = foldl' App
mkTyApps :: Term
-> [Type]
-> Term
mkTyApps = foldl' TyApp
mkTicks
:: Term
-> [TickInfo]
-> Term
mkTicks tm ticks = foldl' (\e s -> Tick s e) tm (nub ticks)
isFun :: TyConMap
-> Term
-> Bool
isFun m t = isFunTy m (termType m t)
isPolyFun :: TyConMap
-> Term
-> Bool
isPolyFun m t = isPolyFunCoreTy m (termType m t)
isLam :: Term
-> Bool
isLam (Lam {}) = True
isLam _ = False
isLet :: Term
-> Bool
isLet (Letrec {}) = True
isLet _ = False
isVar :: Term
-> Bool
isVar (Var {}) = True
isVar _ = False
isLocalVar
:: Term
-> Bool
isLocalVar (Var v) = isLocalId v
isLocalVar _ = False
isCon :: Term
-> Bool
isCon (Data {}) = True
isCon _ = False
isPrim :: Term
-> Bool
isPrim (Prim {}) = True
isPrim _ = False
idToVar :: Id
-> Term
idToVar i@(Id {}) = Var i
idToVar tv = error $ $(curLoc) ++ "idToVar: tyVar: " ++ showPpr tv
varToId :: Term
-> Id
varToId (Var i) = i
varToId e = error $ $(curLoc) ++ "varToId: not a var: " ++ showPpr e
termSize :: Term
-> Word
termSize (Var {}) = 1
termSize (Data {}) = 1
termSize (Literal {}) = 1
termSize (Prim {}) = 1
termSize (Lam _ e) = termSize e + 1
termSize (TyLam _ e) = termSize e
termSize (App e1 e2) = termSize e1 + termSize e2
termSize (TyApp e _) = termSize e
termSize (Cast e _ _) = termSize e
termSize (Tick _ e) = termSize e
termSize (Letrec bndrs e) = sum (bodySz:bndrSzs)
where
bndrSzs = map (termSize . snd) bndrs
bodySz = termSize e
termSize (Case subj _ alts) = sum (subjSz:altSzs)
where
subjSz = termSize subj
altSzs = map (termSize . snd) alts
mkVec :: DataCon
-> DataCon
-> Type
-> Integer
-> [Term]
-> Term
mkVec nilCon consCon resTy = go
where
go _ [] = mkApps (Data nilCon) [Right (LitTy (NumTy 0))
,Right resTy
,Left (primCo nilCoTy)
]
go n (x:xs) = mkApps (Data consCon) [Right (LitTy (NumTy n))
,Right resTy
,Right (LitTy (NumTy (n-1)))
,Left (primCo (consCoTy n))
,Left x
,Left (go (n-1) xs)]
nilCoTy = head (fromJust $! dataConInstArgTys nilCon [(LitTy (NumTy 0))
,resTy])
consCoTy n = head (fromJust $! dataConInstArgTys consCon
[(LitTy (NumTy n))
,resTy
,(LitTy (NumTy (n-1)))])
appendToVec :: DataCon
-> Type
-> Term
-> Integer
-> [Term]
-> Term
appendToVec consCon resTy vec = go
where
go _ [] = vec
go n (x:xs) = mkApps (Data consCon) [Right (LitTy (NumTy n))
,Right resTy
,Right (LitTy (NumTy (n-1)))
,Left (primCo (consCoTy n))
,Left x
,Left (go (n-1) xs)]
consCoTy n = head (fromJust $! dataConInstArgTys consCon
[(LitTy (NumTy n))
,resTy
,(LitTy (NumTy (n-1)))])
availableUniques
:: Term
-> [Unique]
availableUniques t = [ n | n <- [0..] , n `IntSet.notMember` avoid ]
where
avoid = Lens.foldMapOf termFreeVarsX (\a i -> IntSet.insert (varUniq a) i) t
IntSet.empty
extractElems
:: Supply
-> InScopeSet
-> DataCon
-> Type
-> Char
-> Integer
-> Term
-> (Supply, [(Term,[LetBinding])])
extractElems supply inScope consCon resTy s maxN vec =
first fst (go maxN (supply,inScope) vec)
where
go :: Integer -> (Supply,InScopeSet) -> Term
-> ((Supply,InScopeSet),[(Term,[LetBinding])])
go 0 uniqs _ = (uniqs,[])
go n uniqs0 e =
(uniqs3,(elNVar,[(elNId, lhs),(restNId, rhs)]):restVs)
where
tys = [(LitTy (NumTy n)),resTy,(LitTy (NumTy (n-1)))]
(Just idTys) = dataConInstArgTys consCon tys
restTy = last idTys
(uniqs1,mTV) = mkUniqSystemTyVar uniqs0 ("m",typeNatKind)
(uniqs2,[elNId,restNId,co,el,rest]) =
mapAccumR mkUniqSystemId uniqs1 $ zip
["el" `T.append` (s `T.cons` T.pack (show (maxN-n)))
,"rest" `T.append` (s `T.cons` T.pack (show (maxN-n)))
,"_co_"
,"el"
,"rest"
]
(resTy:restTy:idTys)
elNVar = Var elNId
pat = DataPat consCon [mTV] [co,el,rest]
lhs = Case e resTy [(pat,Var el)]
rhs = Case e restTy [(pat,Var rest)]
(uniqs3,restVs) = go (n-1) uniqs2 (Var restNId)
extractTElems
:: Supply
-> InScopeSet
-> DataCon
-> DataCon
-> Type
-> Char
-> Integer
-> Term
-> (Supply,([Term],[LetBinding]))
extractTElems supply inScope lrCon brCon resTy s maxN tree =
first fst (go maxN [0..(2^(maxN+1))-2] [0..(2^maxN - 1)] (supply,inScope) tree)
where
go :: Integer
-> [Int]
-> [Int]
-> (Supply,InScopeSet)
-> Term
-> ((Supply,InScopeSet),([Term],[LetBinding]))
go 0 _ ks uniqs0 e = (uniqs1,([elNVar],[(elNId, rhs)]))
where
tys = [LitTy (NumTy 0),resTy]
(Just idTys) = dataConInstArgTys lrCon tys
(uniqs1,[elNId,co,el]) =
mapAccumR mkUniqSystemId uniqs0 $ zip
[ "el" `T.append` (s `T.cons` T.pack (show (head ks)))
, "_co_"
, "el"
]
(resTy:idTys)
elNVar = Var elNId
pat = DataPat lrCon [] [co,el]
rhs = Case e resTy [(pat,Var el)]
go n bs ks uniqs0 e =
(uniqs4
,(lVars ++ rVars,(ltNId, ltRhs):
(rtNId, rtRhs):
(lBinds ++ rBinds)))
where
tys = [LitTy (NumTy n),resTy,LitTy (NumTy (n-1))]
(Just idTys) = dataConInstArgTys brCon tys
(uniqs1,mTV) = mkUniqSystemTyVar uniqs0 ("m",typeNatKind)
(b0:bL,b1:bR) = splitAt (length bs `div` 2) bs
brTy = last idTys
(uniqs2,[ltNId,rtNId,co,lt,rt]) =
mapAccumR mkUniqSystemId uniqs1 $ zip
["lt" `T.append` (s `T.cons` T.pack (show b0))
,"rt" `T.append` (s `T.cons` T.pack (show b1))
,"_co_"
,"lt"
,"rt"
]
(brTy:brTy:idTys)
ltVar = Var ltNId
rtVar = Var rtNId
pat = DataPat brCon [mTV] [co,lt,rt]
ltRhs = Case e brTy [(pat,Var lt)]
rtRhs = Case e brTy [(pat,Var rt)]
(kL,kR) = splitAt (length ks `div` 2) ks
(uniqs3,(lVars,lBinds)) = go (n-1) bL kL uniqs2 ltVar
(uniqs4,(rVars,rBinds)) = go (n-1) bR kR uniqs3 rtVar
mkRTree :: DataCon
-> DataCon
-> Type
-> Integer
-> [Term]
-> Term
mkRTree lrCon brCon resTy = go
where
go _ [x] = mkApps (Data lrCon) [Right (LitTy (NumTy 0))
,Right resTy
,Left (primCo lrCoTy)
,Left x
]
go n xs =
let (xsL,xsR) = splitAt (length xs `div` 2) xs
in mkApps (Data brCon) [Right (LitTy (NumTy n))
,Right resTy
,Right (LitTy (NumTy (n-1)))
,Left (primCo (brCoTy n))
,Left (go (n-1) xsL)
,Left (go (n-1) xsR)]
lrCoTy = head (fromJust $! dataConInstArgTys lrCon [(LitTy (NumTy 0))
,resTy])
brCoTy n = head (fromJust $! dataConInstArgTys brCon
[(LitTy (NumTy n))
,resTy
,(LitTy (NumTy (n-1)))])
isSignalType :: TyConMap -> Type -> Bool
isSignalType tcm ty = go HashSet.empty ty
where
go tcSeen (tyView -> TyConApp tcNm args) = case nameOcc tcNm of
"Clash.Signal.Internal.Signal" -> True
"Clash.Signal.BiSignal.BiSignalIn" -> True
"Clash.Signal.Internal.BiSignalOut" -> True
_ | tcNm `HashSet.member` tcSeen -> False
| otherwise -> case lookupUniqMap tcNm tcm of
Just tc -> let dcs = tyConDataCons tc
dcInsArgTys = concat
$ mapMaybe (`dataConInstArgTys` args) dcs
tcSeen' = HashSet.insert tcNm tcSeen
in any (go tcSeen') dcInsArgTys
Nothing -> traceIf True ($(curLoc) ++ "isSignalType: " ++ show tcNm
++ " not found.") False
go _ _ = False
isClockOrReset
:: TyConMap
-> Type
-> Bool
isClockOrReset m (coreView1 m -> Just ty) = isClockOrReset m ty
isClockOrReset _ (tyView -> TyConApp tcNm _) = case nameOcc tcNm of
"Clash.Signal.Internal.Clock" -> True
"Clash.Signal.Internal.Reset" -> True
_ -> False
isClockOrReset _ _ = False
tyNatSize :: TyConMap
-> Type
-> Except String Integer
tyNatSize m (coreView1 m -> Just ty) = tyNatSize m ty
tyNatSize _ (LitTy (NumTy i)) = return i
tyNatSize _ ty = throwE $ $(curLoc) ++ "Cannot reduce to an integer:\n" ++ showPpr ty
mkUniqSystemTyVar
:: (Supply, InScopeSet)
-> (OccName, Kind)
-> ((Supply, InScopeSet), TyVar)
mkUniqSystemTyVar (supply,inScope) (nm, ki) =
((supply',extendInScopeSet inScope v'), v')
where
(u,supply') = freshId supply
v = mkTyVar ki (mkUnsafeSystemName nm u)
v' = uniqAway inScope v
mkUniqSystemId
:: (Supply, InScopeSet)
-> (OccName, Type)
-> ((Supply,InScopeSet), Id)
mkUniqSystemId (supply,inScope) (nm, ty) =
((supply',extendInScopeSet inScope v'), v')
where
(u,supply') = freshId supply
v = mkLocalId ty (mkUnsafeSystemName nm u)
v' = uniqAway inScope v
mkUniqInternalId
:: (Supply, InScopeSet)
-> (OccName, Type)
-> ((Supply,InScopeSet), Id)
mkUniqInternalId (supply,inScope) (nm, ty) =
((supply',extendInScopeSet inScope v'), v')
where
(u,supply') = freshId supply
v = mkLocalId ty (mkUnsafeInternalName nm u)
v' = uniqAway inScope v
dataConInstArgTysE
:: HasCallStack
=> InScopeSet
-> TyConMap
-> DataCon
-> [Type]
-> Maybe [Type]
dataConInstArgTysE is0 tcm (MkData { dcArgTys, dcExtTyVars, dcUnivTyVars }) inst_tys = do
let is1 = extendInScopeSetList is0 dcExtTyVars
is2 = unionInScope is1 (mkInScopeSet (tyFVsOfTypes inst_tys))
subst = extendTvSubstList (mkSubst is2) (zip dcUnivTyVars inst_tys)
go
(substGlobalsInExistentials is0 dcExtTyVars (zip dcUnivTyVars inst_tys))
(map (substTy subst) dcArgTys)
where
go
:: [TyVar]
-> [Type]
-> Maybe [Type]
go exts0 args0 =
let eqs = catMaybes (map (typeEq tcm) args0) in
case solveNonAbsurds tcm eqs of
[] ->
Just args0
sols ->
go exts1 args1
where
exts1 = substInExistentialsList is0 exts0 sols
is2 = extendInScopeSetList is0 exts1
subst = extendTvSubstList (mkSubst is2) sols
args1 = map (substTy subst) args0
dataConInstArgTys :: DataCon -> [Type] -> Maybe [Type]
dataConInstArgTys (MkData { dcArgTys, dcUnivTyVars, dcExtTyVars }) inst_tys =
let tyvars = dcUnivTyVars ++ dcExtTyVars in
if length tyvars == length inst_tys then
Just (map (substTyWith tyvars inst_tys) dcArgTys)
else
Nothing
primCo
:: Type
-> Term
primCo ty = Prim "_CO_" (PrimInfo ty WorkNever)
undefinedTm
:: Type
-> Term
undefinedTm = TyApp (Prim "Clash.Transformations.undefined" (PrimInfo undefinedTy WorkNever))
substArgTys
:: DataCon
-> [Type]
-> [Type]
substArgTys dc args =
let univTVs = dcUnivTyVars dc
extTVs = dcExtTyVars dc
argsFVs = foldl' unionVarSet emptyVarSet
(map (Lens.foldMapOf typeFreeVars unitVarSet) args)
is = mkInScopeSet (argsFVs `unionVarSet` mkVarSet extTVs)
subst = extendTvSubstList (mkSubst is) (univTVs `zipEqual` args)
in map (substTy subst) (dcArgTys dc)
stripTicks :: Term -> Term
stripTicks (Tick _ e) = stripTicks e
stripTicks e = e
tySym
:: TyConMap
-> Type
-> Except String String
tySym m (coreView1 m -> Just ty) = tySym m ty
tySym _ (LitTy (SymTy s)) = return s
tySym _ ty = throwE $ $(curLoc) ++ "Cannot reduce to a string:\n" ++ showPpr ty