-- UUAGC 0.9.52.1 (build/103/lib-ehc/UHC/Light/Compiler/Ty/Trf/Quantif) module UHC.Light.Compiler.Ty.Trf.Quantify(tyQuantify , TyQuOpts (..), defaultTyQuOpts , TyQuOut (..) , tyQuantifyOuter , tyKiQuantify, valTyQuantify , tyQuantifyClosed, tyQuantifyRank, tyQuantifyRank') where import UHC.Util.Utils import UHC.Light.Compiler.Base.HsName.Builtin import UHC.Light.Compiler.Base.Common import UHC.Light.Compiler.Ty import UHC.Light.Compiler.VarMp import UHC.Light.Compiler.Substitutable import qualified Data.Set as Set import qualified Data.Map as Map import Data.List as List import Data.Maybe import UHC.Util.Utils import UHC.Util.Pretty tvarSOccurCount :: [TyVarIdS] -> AssocL TyVarId Int tvarSOccurCount = map (\vl@(v:_) -> (v,length vl)) . group . sort . concat . map Set.toList tvarSOccurGE2 :: [TyVarIdS] -> TyVarIdS tvarSOccurGE2 = Set.fromList . map fst . filter ((>1).snd) . tvarSOccurCount data TyQuCtxt = TyQuCtxtArrow | TyQuCtxtProd | TyQuCtxtOnTop | TyQuCtxtOther deriving (Show,Eq) {-| There are some conventions/restrictions on the structure of types that are not enforced by the abstract syntax: Encoding of prove-constraints: concrete syntax: {! impls !} -> ty abstract syntax: Ty_App (Ty_App (Ty_Con "->") (Ty_Impls impls)) ty Encoding of assume-constraints: concrete syntax: (ty, {! pred1 !}, ..., {! predn !}) abstract syntax: Ty_Ext (... (Ty_Ext ty (prod m+1) (Ty_Pred pred_1) ) ...) (prod m+n) (Ty_Pred pred_n) In other words: the predicates are at the outset of a product, pred_n "more outermost" than pred_{n-1}. -} {-| The basic alternatives encode the following: - Con: data type constructors, including tuple constructors - App: application to 1 argument, for example 'a -> b' is encoded as (App (App -> a) b) - Any: representing Bot/Top depending on context: (1) unknown expected type, (2) error type - Var: type variables, including a category: plain tyvars, fixed tyvars (aka skolems) -} tyQuantifyClosed :: Ty -> Ty tyQuantifyClosed = tyQuantifyRank [1..] tyQuantifyRank' :: TvIsBound -> [Int] -> Ty -> Ty tyQuantifyRank' tvIsBound rL ty = tqoTy (tyQuantifyWithOpts (defaultTyQuOpts {tqoptQuRanks = rL, tqoptBaseQuant = tyQu_Forall, tqoptTvIsBound = tvIsBound}) ty) tyQuantifyRank :: [Int] -> Ty -> Ty tyQuantifyRank = tyQuantifyRank' (const False) tyQuantify :: TvIsBound -> Ty -> Ty tyQuantify tvIsBound ty = tyQuantify' tvIsBound tyQu_Forall ty tyQuantifyOuter :: (TyVarId -> Ty) -> TvIsBound -> Ty -> Ty tyQuantifyOuter tvKi tvIsBound ty = tqoTy tqo where tqo = tyQuantifyWithOpts (defaultTyQuOpts { tqoptAllowInnerQuant = False , tqoptTvIsBound = tvIsBound , tqoptBaseQuant = tyQu_Forall , tqoptTvL1 = tvKi } ) ty -- | Quantify kind, i.e. add universal quantifier for free tvars when kind polymorphism is allowed, otherwise just * tyKiQuantify :: Bool -- ^ kind polymorphism on (for inference steered by PolyKinds pragma) -> TvIsBound -> Ty -> Ty tyKiQuantify polyKinds tvIsBound ty -- = tyQuantify' tvIsBound tyQu_Forall {- tyQu_KiForall -} ty = tqoTy $ tyQuantifyWithOpts opts ty where opts = defaultTyQuOpts { tqoptAllowInnerQuant = False , tqoptTvIsBound = tvIsBound , tqoptBaseQuant = tyQu_Forall , tqoptQuantVarDefaultsTo = if polyKinds then Nothing else Just kiStar } valTyQuantify :: (TyVarId -> Ty) -> TvIsBound -> Ty -> Ty valTyQuantify tvKi tvIsBound ty = tqoTy $ tyQuantifyWithOpts opts ty where opts = defaultTyQuOpts { tqoptAllowInnerQuant = False , tqoptTvIsBound = tvIsBound , tqoptTvL1 = tvKi } tyQuantify' :: TvIsBound -> TyQu -> Ty -> Ty tyQuantify' tvIsBound baseQuant ty = tqoTy tqo where tqo = tyQuantifyWithOpts (defaultTyQuOpts { tqoptTvIsBound = tvIsBound , tqoptBaseQuant = baseQuant } ) ty data TyQuOpts = TyQuOpts { tqoptTvIsBound :: TvIsBound , tqoptQuantVarDefaultsTo :: !(Maybe Ty) -- ^ if provided, not quantification takes place but var defaults to this , tqoptAllowInnerQuant :: !Bool , tqoptBaseQuant :: !TyQu , tqoptTvL1 :: TyVarId -> Ty -- ^ mapping of tvar to 1 higher metalevel ty (i.e. kind) , tqoptQuRanks :: [Int] } defaultTyQuOpts :: TyQuOpts defaultTyQuOpts = TyQuOpts (const False) Nothing True tyQu_Forall (const kiStar) [1..] data TyQuOut = TyQuOut { tqoTy :: Ty } tyQuantifyWithOpts :: TyQuOpts -> Ty -> TyQuOut tyQuantifyWithOpts opts ty = let t = wrap_TyAGItf (sem_TyAGItf (TyAGItf_AGItf ty)) (Inh_TyAGItf { opts_Inh_TyAGItf = opts , baseQu_Inh_TyAGItf = tqoptBaseQuant opts }) in TyQuOut { tqoTy = quTy_Syn_TyAGItf t } type TvIsBound = TyVarId -> Bool type TvLevIsBound = MetaLev -> TvIsBound tvIsBound2L :: MetaLev -> TvIsBound -> TvLevIsBound tvIsBound2L mlev b = \mlev' -> if mlev' == mlev then b else const False tvIsBound2L0, tvIsBound2L1 :: TvIsBound -> TvLevIsBound tvIsBound2L0 = tvIsBound2L 0 tvIsBound2L1 = tvIsBound2L 1 type TyVarIdsToBind = AssocL TyVarId Ty tvBoundAddS :: MetaLev -> TyVarIdS -> TvLevIsBound -> TvLevIsBound tvBoundAddS mlev tvS tvIsBound = \mlev' v -> (mlev == mlev' && v `Set.member` tvS) || tvIsBound mlev' v tvNotBound :: MetaLev -> TvLevIsBound -> TyVarIdS -> TyVarIdS tvNotBound mlev tvIsBound = Set.filter (\tv -> not (tvIsBound mlev tv)) tvarsToQuantL1 :: TyVarIdsToBind -> TvLevIsBound -> (TyVarIdsToBind,TyVarIdS,TvLevIsBound) tvarsToQuantL1 boundablesL tvIsBound = (boundablesL1L,boundablesL1S,tvBoundAddS 1 boundablesL1S tvIsBound) where boundablesL1S = tvNotBound 1 tvIsBound $ Set.unions [ varFreeSet l1 | (_,l1) <- boundablesL ] boundablesL1L = [ (v,kiStar) | v <- Set.toList boundablesL1S ] -- | Compute bindable tvars tvarsToQuant :: TyQuOpts -> Bool -> TvCatMp -> (TyVarId -> Bool) -> TvLevIsBound -- ^ 'is already bound?' -> TyVarIdS -> ( TyVarIdsToBind -- to bind universal, on this level , TyVarIdsToBind -- to bind existential , TyVarIdsToBind -- to bind universal, 1 level higher , TvLevIsBound -- updated 'is already bound?' , VarMp -- the tvars which are defaulted ) tvarsToQuant opts isQuLoc _ mayQuFx tvIsBound tvS = if isQuLoc then let boundablesS = tvNotBound 0 tvIsBound tvS (boundablesL,boundablesL1L,tvIsBound',defaultedVarMp) | isJust mbDf = ([] , [] , tvIsBound, assocTyLToVarMp [ (v,df) | (v,_) <- boundablesL ]) | otherwise = (boundablesL, b1L, isb , emptyVarMp ) where mbDf@(~(Just df)) = tqoptQuantVarDefaultsTo opts (b1L,_,isb) = tvarsToQuantL1 boundablesL (tvBoundAddS 0 boundablesS tvIsBound) boundablesL = [ (v, tqoptTvL1 opts v) | v <- Set.toList boundablesS ] in ( boundablesL , [] , boundablesL1L , tvIsBound' , defaultedVarMp ) else ([],[],[],tvIsBound,emptyVarMp) tvMayQuFx :: TyQu -> TvCatMp -> Bool -> TyVarId -> Bool tvMayQuFx qu fxTvM isQuFxLoc tv = False -- isQuFxLoc -- True mkTyQuEx :: TyQuOpts -> TyQu -> TyVarIdsToBind -> TyVarIdsToBind-> TyVarIdsToBind -> Ty -> Ty mkTyQuEx opts q tvsL1 tvs tvsEx t = mkTyQu (TyQu_Forall (tyquMetaLev q + 1)) tvsL1 $ mkTyQu q tvs $ mkTyQu (tyquExists q) tvsEx t mkTyQuForRank :: TyQuOpts -> Bool -> TyQu -> TyVarIdsToBind -> TyVarIdsToBind -> TyVarIdsToBind -> Ty -> Ty mkTyQuForRank opts allow q tvsL1 tvs tvsEx t | allow = mkTyQuEx opts q tvsL1 tvs tvsEx t | otherwise = t -- Impls ------------------------------------------------------- {- visit 0: inherited attributes: isAtTop : Bool opts : TyQuOpts pol : Polarity synthesized attributes: frTvSL : [TyVarIdS] gathFxTvM : TvCatMp qInsideTvS : TyVarIdS qOrphanTvS : TyVarIdS visit 1: inherited attributes: baseQu : TyQu defaultedVarMp : VarMp fxTvM : TvCatMp isRow : Bool qSurrTvS : TyVarIdS rank : Int tvIsBound : TvLevIsBound tyCtxt : TyQuCtxt synthesized attributes: quTy : Impls self : Impls alternatives: alternative Tail: child iv : {ImplsVarId} child proveOccs : {[ImplsProveOcc]} visit 1: local quTy : _ local self : _ alternative Cons: child iv : {ImplsVarId} child pr : Pred child pv : {PredOccId} child prange : {Range} child proveOccs : {[ImplsProveOcc]} child tl : Impls visit 1: local quTy : _ local self : _ alternative Nil: visit 1: local quTy : _ local self : _ -} -- cata sem_Impls :: Impls -> T_Impls sem_Impls (Impls_Tail _iv _proveOccs) = (sem_Impls_Tail _iv _proveOccs) sem_Impls (Impls_Cons _iv _pr _pv _prange _proveOccs _tl) = (sem_Impls_Cons _iv (sem_Pred _pr) _pv _prange _proveOccs (sem_Impls _tl)) sem_Impls (Impls_Nil) = (sem_Impls_Nil) -- semantic domain type T_Impls = Bool -> TyQuOpts -> Polarity -> ( ([TyVarIdS]),TvCatMp,TyVarIdS,TyVarIdS,T_Impls_1) type T_Impls_1 = TyQu -> VarMp -> TvCatMp -> Bool -> TyVarIdS -> Int -> TvLevIsBound -> TyQuCtxt -> ( Impls,Impls) sem_Impls_Tail :: ImplsVarId -> ([ImplsProveOcc]) -> T_Impls sem_Impls_Tail iv_ proveOccs_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case ([]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (Set.empty) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Impls_Tail_1 :: T_Impls_1 sem_Impls_Tail_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (Impls_Tail iv_ proveOccs_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Impls_Tail iv_ proveOccs_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_Impls_Tail_1)) of { ( sem_Impls_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Impls_1) }) }) }) }) })) sem_Impls_Cons :: ImplsVarId -> T_Pred -> PredOccId -> Range -> ([ImplsProveOcc]) -> T_Impls -> T_Impls sem_Impls_Cons iv_ pr_ pv_ prange_ proveOccs_ tl_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (_lhsIpol) of { _tlOpol -> (case (_lhsIopts) of { _tlOopts -> (case (_lhsIisAtTop) of { _tlOisAtTop -> (case (tl_ _tlOisAtTop _tlOopts _tlOpol) of { ( _tlIfrTvSL,_tlIgathFxTvM,_tlIqInsideTvS,_tlIqOrphanTvS,tl_1) -> (case (_lhsIpol) of { _prOpol -> (case (_lhsIopts) of { _prOopts -> (case (_lhsIisAtTop) of { _prOisAtTop -> (case (pr_ _prOisAtTop _prOopts _prOpol) of { ( _prIfrTvSL,_prIgathFxTvM,_prIqInsideTvS,_prIqOrphanTvS,pr_1) -> (case (_prIfrTvSL ++ _tlIfrTvSL) of { _lhsOfrTvSL -> (case (_prIgathFxTvM `Map.union` _tlIgathFxTvM) of { _lhsOgathFxTvM -> (case (_prIqInsideTvS `Set.union` _tlIqInsideTvS) of { _lhsOqInsideTvS -> (case (_prIqOrphanTvS `Set.union` _tlIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Impls_Cons_1 :: T_Impls_1 sem_Impls_Cons_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _tlOtyCtxt -> (case (_lhsItvIsBound) of { _tlOtvIsBound -> (case (_lhsIrank) of { _tlOrank -> (case (_lhsIfxTvM) of { _tlOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tlOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tlObaseQu -> (case (_lhsItyCtxt) of { _prOtyCtxt -> (case (_lhsItvIsBound) of { _prOtvIsBound -> (case (_lhsIrank) of { _prOrank -> (case (_lhsIfxTvM) of { _prOfxTvM -> (case (_lhsIdefaultedVarMp) of { _prOdefaultedVarMp -> (case (_lhsIbaseQu) of { _prObaseQu -> (case (_lhsIqSurrTvS) of { _tlOqSurrTvS -> (case (_lhsIisRow) of { _tlOisRow -> (case (tl_1 _tlObaseQu _tlOdefaultedVarMp _tlOfxTvM _tlOisRow _tlOqSurrTvS _tlOrank _tlOtvIsBound _tlOtyCtxt) of { ( _tlIquTy,_tlIself) -> (case (_lhsIqSurrTvS) of { _prOqSurrTvS -> (case (_lhsIisRow) of { _prOisRow -> (case (pr_1 _prObaseQu _prOdefaultedVarMp _prOfxTvM _prOisRow _prOqSurrTvS _prOrank _prOtvIsBound _prOtyCtxt) of { ( _prIquTy,_prIself) -> (case (Impls_Cons iv_ _prIquTy pv_ prange_ proveOccs_ _tlIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Impls_Cons iv_ _prIself pv_ prange_ proveOccs_ _tlIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Impls_Cons_1)) of { ( sem_Impls_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Impls_1) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Impls_Nil :: T_Impls sem_Impls_Nil = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case ([]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (Set.empty) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Impls_Nil_1 :: T_Impls_1 sem_Impls_Nil_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (Impls_Nil) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Impls_Nil) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_Impls_Nil_1)) of { ( sem_Impls_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Impls_1) }) }) }) }) })) -- Label ------------------------------------------------------- {- visit 0: synthesized attributes: quTy : Label self : Label alternatives: alternative Lab: child nm : {HsName} visit 0: local quTy : _ local self : _ alternative Var: child lv : {LabelVarId} visit 0: local quTy : _ local self : _ -} -- cata sem_Label :: Label -> T_Label sem_Label (Label_Lab _nm) = (sem_Label_Lab _nm) sem_Label (Label_Var _lv) = (sem_Label_Var _lv) -- semantic domain type T_Label = ( Label,Label) sem_Label_Lab :: HsName -> T_Label sem_Label_Lab nm_ = (case (Label_Lab nm_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Label_Lab nm_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) sem_Label_Var :: LabelVarId -> T_Label sem_Label_Var lv_ = (case (Label_Var lv_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Label_Var lv_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) -- LabelAGItf -------------------------------------------------- {- alternatives: alternative AGItf: child lab : Label -} -- cata sem_LabelAGItf :: LabelAGItf -> T_LabelAGItf sem_LabelAGItf (LabelAGItf_AGItf _lab) = (sem_LabelAGItf_AGItf (sem_Label _lab)) -- semantic domain type T_LabelAGItf = ( ) sem_LabelAGItf_AGItf :: T_Label -> T_LabelAGItf sem_LabelAGItf_AGItf lab_ = ( ) -- Pred -------------------------------------------------------- {- visit 0: inherited attributes: isAtTop : Bool opts : TyQuOpts pol : Polarity synthesized attributes: frTvSL : [TyVarIdS] gathFxTvM : TvCatMp qInsideTvS : TyVarIdS qOrphanTvS : TyVarIdS visit 1: inherited attributes: baseQu : TyQu defaultedVarMp : VarMp fxTvM : TvCatMp isRow : Bool qSurrTvS : TyVarIdS rank : Int tvIsBound : TvLevIsBound tyCtxt : TyQuCtxt synthesized attributes: quTy : Pred self : Pred alternatives: alternative Class: child ty : Ty visit 0: local appSpinePos : _ visit 1: local quTy : _ local self : _ alternative Pred: child ty : Ty visit 0: local appSpinePos : _ visit 1: local quTy : _ local self : _ alternative Lacks: child ty : Ty child lab : Label visit 0: local appSpinePos : _ visit 1: local quTy : _ local self : _ alternative Arrow: child args : PredSeq child res : Pred visit 1: local appSpinePos : _ local quTy : _ local self : _ alternative Eq: child tyL : Ty child tyR : Ty visit 0: local appSpinePos : _ visit 1: local quTy : _ local self : _ alternative Var: child pv : {TyVarId} visit 1: local quTy : _ local self : _ alternative Preds: child seq : PredSeq visit 1: local appSpinePos : _ local quTy : _ local self : _ -} -- cata sem_Pred :: Pred -> T_Pred sem_Pred (Pred_Class _ty) = (sem_Pred_Class (sem_Ty _ty)) sem_Pred (Pred_Pred _ty) = (sem_Pred_Pred (sem_Ty _ty)) sem_Pred (Pred_Lacks _ty _lab) = (sem_Pred_Lacks (sem_Ty _ty) (sem_Label _lab)) sem_Pred (Pred_Arrow _args _res) = (sem_Pred_Arrow (sem_PredSeq _args) (sem_Pred _res)) sem_Pred (Pred_Eq _tyL _tyR) = (sem_Pred_Eq (sem_Ty _tyL) (sem_Ty _tyR)) sem_Pred (Pred_Var _pv) = (sem_Pred_Var _pv) sem_Pred (Pred_Preds _seq) = (sem_Pred_Preds (sem_PredSeq _seq)) -- semantic domain type T_Pred = Bool -> TyQuOpts -> Polarity -> ( ([TyVarIdS]),TvCatMp,TyVarIdS,TyVarIdS,T_Pred_1) type T_Pred_1 = TyQu -> VarMp -> TvCatMp -> Bool -> TyVarIdS -> Int -> TvLevIsBound -> TyQuCtxt -> ( Pred,Pred) sem_Pred_Class :: T_Ty -> T_Pred sem_Pred_Class ty_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (0) of { _appSpinePos -> (case (_appSpinePos) of { _tyOappSpinePos -> (case (_lhsIopts) of { _tyOopts -> (case (_lhsIisAtTop) of { _tyOisAtTop -> (case (polInvariant) of { _tyOpol -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (_tyIfrTvSL) of { _lhsOfrTvSL -> (case (_tyIgathFxTvM) of { _lhsOgathFxTvM -> (case (_tyIqInsideTvS) of { _lhsOqInsideTvS -> (case (_tyIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Pred_Class_1 :: T_Pred_1 sem_Pred_Class_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _tyOtyCtxt -> (case (_lhsItvIsBound) of { _tyOtvIsBound -> (case (_lhsIrank) of { _tyOrank -> (case (_lhsIfxTvM) of { _tyOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (_lhsIqSurrTvS) of { _tyOqSurrTvS -> (case (_lhsIisRow) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (Pred_Class _tyIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Pred_Class _tyIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Pred_Class_1)) of { ( sem_Pred_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Pred_1) }) }) }) }) }) }) }) }) }) }) })) sem_Pred_Pred :: T_Ty -> T_Pred sem_Pred_Pred ty_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (0) of { _appSpinePos -> (case (_appSpinePos) of { _tyOappSpinePos -> (case (_lhsIopts) of { _tyOopts -> (case (_lhsIisAtTop) of { _tyOisAtTop -> (case (polCovariant) of { _tyOpol -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (_tyIfrTvSL) of { _lhsOfrTvSL -> (case (_tyIgathFxTvM) of { _lhsOgathFxTvM -> (case (_tyIqInsideTvS) of { _lhsOqInsideTvS -> (case (_tyIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Pred_Pred_1 :: T_Pred_1 sem_Pred_Pred_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _tyOtyCtxt -> (case (_lhsItvIsBound) of { _tyOtvIsBound -> (case (_lhsIrank) of { _tyOrank -> (case (_lhsIfxTvM) of { _tyOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (_lhsIqSurrTvS) of { _tyOqSurrTvS -> (case (_lhsIisRow) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (Pred_Pred _tyIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Pred_Pred _tyIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Pred_Pred_1)) of { ( sem_Pred_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Pred_1) }) }) }) }) }) }) }) }) }) }) })) sem_Pred_Lacks :: T_Ty -> T_Label -> T_Pred sem_Pred_Lacks ty_ lab_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (0) of { _appSpinePos -> (case (_appSpinePos) of { _tyOappSpinePos -> (case (_lhsIpol) of { _tyOpol -> (case (_lhsIopts) of { _tyOopts -> (case (_lhsIisAtTop) of { _tyOisAtTop -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (_tyIfrTvSL) of { _lhsOfrTvSL -> (case (_tyIgathFxTvM) of { _lhsOgathFxTvM -> (case (_tyIqInsideTvS) of { _lhsOqInsideTvS -> (case (_tyIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Pred_Lacks_1 :: T_Pred_1 sem_Pred_Lacks_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _tyOtyCtxt -> (case (_lhsItvIsBound) of { _tyOtvIsBound -> (case (_lhsIrank) of { _tyOrank -> (case (_lhsIfxTvM) of { _tyOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (lab_) of { ( _labIquTy,_labIself) -> (case (_lhsIqSurrTvS) of { _tyOqSurrTvS -> (case (_lhsIisRow) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (Pred_Lacks _tyIquTy _labIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Pred_Lacks _tyIself _labIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Pred_Lacks_1)) of { ( sem_Pred_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Pred_1) }) }) }) }) }) }) }) }) }) }) })) sem_Pred_Arrow :: T_PredSeq -> T_Pred -> T_Pred sem_Pred_Arrow args_ res_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (_lhsIpol) of { _resOpol -> (case (_lhsIopts) of { _resOopts -> (case (_lhsIisAtTop) of { _resOisAtTop -> (case (res_ _resOisAtTop _resOopts _resOpol) of { ( _resIfrTvSL,_resIgathFxTvM,_resIqInsideTvS,_resIqOrphanTvS,res_1) -> (case (_lhsIpol) of { _argsOpol -> (case (_lhsIopts) of { _argsOopts -> (case (_lhsIisAtTop) of { _argsOisAtTop -> (case (args_ _argsOisAtTop _argsOopts _argsOpol) of { ( _argsIfrTvSL,_argsIgathFxTvM,_argsIqInsideTvS,args_1) -> (case (_argsIfrTvSL ++ _resIfrTvSL) of { _lhsOfrTvSL -> (case (_argsIgathFxTvM `Map.union` _resIgathFxTvM) of { _lhsOgathFxTvM -> (case (_argsIqInsideTvS `Set.union` _resIqInsideTvS) of { _lhsOqInsideTvS -> (case (_resIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Pred_Arrow_1 :: T_Pred_1 sem_Pred_Arrow_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _resOtyCtxt -> (case (_lhsItvIsBound) of { _resOtvIsBound -> (case (_lhsIrank) of { _resOrank -> (case (_lhsIfxTvM) of { _resOfxTvM -> (case (_lhsIdefaultedVarMp) of { _resOdefaultedVarMp -> (case (_lhsIbaseQu) of { _resObaseQu -> (case (_lhsItyCtxt) of { _argsOtyCtxt -> (case (_lhsItvIsBound) of { _argsOtvIsBound -> (case (_lhsIrank) of { _argsOrank -> (case (_lhsIfxTvM) of { _argsOfxTvM -> (case (_lhsIdefaultedVarMp) of { _argsOdefaultedVarMp -> (case (_lhsIbaseQu) of { _argsObaseQu -> (case (_lhsIqSurrTvS) of { _resOqSurrTvS -> (case (_lhsIisRow) of { _resOisRow -> (case (res_1 _resObaseQu _resOdefaultedVarMp _resOfxTvM _resOisRow _resOqSurrTvS _resOrank _resOtvIsBound _resOtyCtxt) of { ( _resIquTy,_resIself) -> (case (_lhsIqSurrTvS) of { _argsOqSurrTvS -> (case (_lhsIisRow) of { _argsOisRow -> (case (0) of { _appSpinePos -> (case (_appSpinePos) of { _argsOappSpinePos -> (case (args_1 _argsOappSpinePos _argsObaseQu _argsOdefaultedVarMp _argsOfxTvM _argsOisRow _argsOqSurrTvS _argsOrank _argsOtvIsBound _argsOtyCtxt) of { ( _argsIquTy,_argsIself) -> (case (Pred_Arrow _argsIquTy _resIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Pred_Arrow _argsIself _resIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Pred_Arrow_1)) of { ( sem_Pred_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Pred_1) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Pred_Eq :: T_Ty -> T_Ty -> T_Pred sem_Pred_Eq tyL_ tyR_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (0) of { _appSpinePos -> (case (_appSpinePos) of { _tyROappSpinePos -> (case (_appSpinePos) of { _tyLOappSpinePos -> (case (_lhsIpol) of { _tyROpol -> (case (_lhsIopts) of { _tyROopts -> (case (_lhsIisAtTop) of { _tyROisAtTop -> (case (tyR_ _tyROappSpinePos _tyROisAtTop _tyROopts _tyROpol) of { ( _tyRIappFunNm,_tyRIfrTvSL,_tyRIgathFxTvM,_tyRIisArrow,_tyRIisPred,_tyRIisQuLoc,_tyRIqInsideTvS,_tyRIqOrphanTvS,tyR_1) -> (case (_lhsIpol) of { _tyLOpol -> (case (_lhsIopts) of { _tyLOopts -> (case (_lhsIisAtTop) of { _tyLOisAtTop -> (case (tyL_ _tyLOappSpinePos _tyLOisAtTop _tyLOopts _tyLOpol) of { ( _tyLIappFunNm,_tyLIfrTvSL,_tyLIgathFxTvM,_tyLIisArrow,_tyLIisPred,_tyLIisQuLoc,_tyLIqInsideTvS,_tyLIqOrphanTvS,tyL_1) -> (case (_tyLIfrTvSL ++ _tyRIfrTvSL) of { _lhsOfrTvSL -> (case (_tyLIgathFxTvM `Map.union` _tyRIgathFxTvM) of { _lhsOgathFxTvM -> (case (_tyLIqInsideTvS `Set.union` _tyRIqInsideTvS) of { _lhsOqInsideTvS -> (case (_tyRIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Pred_Eq_1 :: T_Pred_1 sem_Pred_Eq_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _tyROtyCtxt -> (case (_lhsItvIsBound) of { _tyROtvIsBound -> (case (_lhsIrank) of { _tyROrank -> (case (_lhsIfxTvM) of { _tyROfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyROdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyRObaseQu -> (case (_lhsItyCtxt) of { _tyLOtyCtxt -> (case (_lhsItvIsBound) of { _tyLOtvIsBound -> (case (_lhsIrank) of { _tyLOrank -> (case (_lhsIfxTvM) of { _tyLOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyLOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyLObaseQu -> (case (_lhsIqSurrTvS) of { _tyROqSurrTvS -> (case (_lhsIisRow) of { _tyROisRow -> (case (tyR_1 _tyRObaseQu _tyROdefaultedVarMp _tyROfxTvM _tyROisRow _tyROqSurrTvS _tyROrank _tyROtvIsBound _tyROtyCtxt) of { ( _tyRIquTy,_tyRIself) -> (case (_lhsIqSurrTvS) of { _tyLOqSurrTvS -> (case (_lhsIisRow) of { _tyLOisRow -> (case (tyL_1 _tyLObaseQu _tyLOdefaultedVarMp _tyLOfxTvM _tyLOisRow _tyLOqSurrTvS _tyLOrank _tyLOtvIsBound _tyLOtyCtxt) of { ( _tyLIquTy,_tyLIself) -> (case (Pred_Eq _tyLIquTy _tyRIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Pred_Eq _tyLIself _tyRIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Pred_Eq_1)) of { ( sem_Pred_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Pred_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Pred_Var :: TyVarId -> T_Pred sem_Pred_Var pv_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case ([]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (Set.empty) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Pred_Var_1 :: T_Pred_1 sem_Pred_Var_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (Pred_Var pv_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Pred_Var pv_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_Pred_Var_1)) of { ( sem_Pred_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Pred_1) }) }) }) }) })) sem_Pred_Preds :: T_PredSeq -> T_Pred sem_Pred_Preds seq_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (_lhsIpol) of { _seqOpol -> (case (_lhsIopts) of { _seqOopts -> (case (_lhsIisAtTop) of { _seqOisAtTop -> (case (seq_ _seqOisAtTop _seqOopts _seqOpol) of { ( _seqIfrTvSL,_seqIgathFxTvM,_seqIqInsideTvS,seq_1) -> (case (_seqIfrTvSL) of { _lhsOfrTvSL -> (case (_seqIgathFxTvM) of { _lhsOgathFxTvM -> (case (_seqIqInsideTvS) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Pred_Preds_1 :: T_Pred_1 sem_Pred_Preds_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _seqOtyCtxt -> (case (_lhsItvIsBound) of { _seqOtvIsBound -> (case (_lhsIrank) of { _seqOrank -> (case (_lhsIfxTvM) of { _seqOfxTvM -> (case (_lhsIdefaultedVarMp) of { _seqOdefaultedVarMp -> (case (_lhsIbaseQu) of { _seqObaseQu -> (case (_lhsIqSurrTvS) of { _seqOqSurrTvS -> (case (_lhsIisRow) of { _seqOisRow -> (case (0) of { _appSpinePos -> (case (_appSpinePos) of { _seqOappSpinePos -> (case (seq_1 _seqOappSpinePos _seqObaseQu _seqOdefaultedVarMp _seqOfxTvM _seqOisRow _seqOqSurrTvS _seqOrank _seqOtvIsBound _seqOtyCtxt) of { ( _seqIquTy,_seqIself) -> (case (Pred_Preds _seqIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Pred_Preds _seqIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Pred_Preds_1)) of { ( sem_Pred_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Pred_1) }) }) }) }) }) }) }) }) })) -- PredSeq ----------------------------------------------------- {- visit 0: inherited attributes: isAtTop : Bool opts : TyQuOpts pol : Polarity synthesized attributes: frTvSL : [TyVarIdS] gathFxTvM : TvCatMp qInsideTvS : TyVarIdS visit 1: inherited attributes: appSpinePos : Int baseQu : TyQu defaultedVarMp : VarMp fxTvM : TvCatMp isRow : Bool qSurrTvS : TyVarIdS rank : Int tvIsBound : TvLevIsBound tyCtxt : TyQuCtxt synthesized attributes: quTy : PredSeq self : PredSeq alternatives: alternative Cons: child hd : Pred child tl : PredSeq visit 1: local quTy : _ local self : _ alternative Nil: visit 1: local quTy : _ local self : _ alternative Var: child av : {TyVarId} visit 1: local quTy : _ local self : _ -} -- cata sem_PredSeq :: PredSeq -> T_PredSeq sem_PredSeq (PredSeq_Cons _hd _tl) = (sem_PredSeq_Cons (sem_Pred _hd) (sem_PredSeq _tl)) sem_PredSeq (PredSeq_Nil) = (sem_PredSeq_Nil) sem_PredSeq (PredSeq_Var _av) = (sem_PredSeq_Var _av) -- semantic domain type T_PredSeq = Bool -> TyQuOpts -> Polarity -> ( ([TyVarIdS]),TvCatMp,TyVarIdS,T_PredSeq_1) type T_PredSeq_1 = Int -> TyQu -> VarMp -> TvCatMp -> Bool -> TyVarIdS -> Int -> TvLevIsBound -> TyQuCtxt -> ( PredSeq,PredSeq) sem_PredSeq_Cons :: T_Pred -> T_PredSeq -> T_PredSeq sem_PredSeq_Cons hd_ tl_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case (_lhsIpol) of { _tlOpol -> (case (_lhsIopts) of { _tlOopts -> (case (_lhsIisAtTop) of { _tlOisAtTop -> (case (tl_ _tlOisAtTop _tlOopts _tlOpol) of { ( _tlIfrTvSL,_tlIgathFxTvM,_tlIqInsideTvS,tl_1) -> (case (_lhsIpol) of { _hdOpol -> (case (_lhsIopts) of { _hdOopts -> (case (_lhsIisAtTop) of { _hdOisAtTop -> (case (hd_ _hdOisAtTop _hdOopts _hdOpol) of { ( _hdIfrTvSL,_hdIgathFxTvM,_hdIqInsideTvS,_hdIqOrphanTvS,hd_1) -> (case (_hdIfrTvSL ++ _tlIfrTvSL) of { _lhsOfrTvSL -> (case (_hdIgathFxTvM `Map.union` _tlIgathFxTvM) of { _lhsOgathFxTvM -> (case (_hdIqInsideTvS `Set.union` _tlIqInsideTvS) of { _lhsOqInsideTvS -> (case ((let sem_PredSeq_Cons_1 :: T_PredSeq_1 sem_PredSeq_Cons_1 = (\ _lhsIappSpinePos _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (_lhsItyCtxt) of { _tlOtyCtxt -> (case (_lhsItvIsBound) of { _tlOtvIsBound -> (case (_lhsIrank) of { _tlOrank -> (case (_lhsIfxTvM) of { _tlOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tlOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tlObaseQu -> (case (_lhsItyCtxt) of { _hdOtyCtxt -> (case (_lhsItvIsBound) of { _hdOtvIsBound -> (case (_lhsIrank) of { _hdOrank -> (case (_lhsIfxTvM) of { _hdOfxTvM -> (case (_lhsIdefaultedVarMp) of { _hdOdefaultedVarMp -> (case (_lhsIbaseQu) of { _hdObaseQu -> (case (_lhsIqSurrTvS) of { _tlOqSurrTvS -> (case (_lhsIisRow) of { _tlOisRow -> (case (_lhsIappSpinePos + 1) of { _tlOappSpinePos -> (case (tl_1 _tlOappSpinePos _tlObaseQu _tlOdefaultedVarMp _tlOfxTvM _tlOisRow _tlOqSurrTvS _tlOrank _tlOtvIsBound _tlOtyCtxt) of { ( _tlIquTy,_tlIself) -> (case (_lhsIqSurrTvS) of { _hdOqSurrTvS -> (case (_lhsIisRow) of { _hdOisRow -> (case (hd_1 _hdObaseQu _hdOdefaultedVarMp _hdOfxTvM _hdOisRow _hdOqSurrTvS _hdOrank _hdOtvIsBound _hdOtyCtxt) of { ( _hdIquTy,_hdIself) -> (case (PredSeq_Cons _hdIquTy _tlIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (PredSeq_Cons _hdIself _tlIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_PredSeq_Cons_1)) of { ( sem_PredSeq_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,sem_PredSeq_1) }) }) }) }) }) }) }) }) }) }) }) })) sem_PredSeq_Nil :: T_PredSeq sem_PredSeq_Nil = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case ([]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (Set.empty) of { _lhsOqInsideTvS -> (case ((let sem_PredSeq_Nil_1 :: T_PredSeq_1 sem_PredSeq_Nil_1 = (\ _lhsIappSpinePos _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (PredSeq_Nil) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (PredSeq_Nil) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_PredSeq_Nil_1)) of { ( sem_PredSeq_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,sem_PredSeq_1) }) }) }) })) sem_PredSeq_Var :: TyVarId -> T_PredSeq sem_PredSeq_Var av_ = (\ _lhsIisAtTop _lhsIopts _lhsIpol -> (case ([]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (Set.empty) of { _lhsOqInsideTvS -> (case ((let sem_PredSeq_Var_1 :: T_PredSeq_1 sem_PredSeq_Var_1 = (\ _lhsIappSpinePos _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (PredSeq_Var av_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (PredSeq_Var av_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_PredSeq_Var_1)) of { ( sem_PredSeq_1) -> ( _lhsOfrTvSL,_lhsOgathFxTvM,_lhsOqInsideTvS,sem_PredSeq_1) }) }) }) })) -- Ty ---------------------------------------------------------- {- visit 0: inherited attributes: appSpinePos : Int isAtTop : Bool opts : TyQuOpts pol : Polarity synthesized attributes: appFunNm : HsName frTvSL : [TyVarIdS] gathFxTvM : TvCatMp isArrow : Bool isPred : Bool isQuLoc : Bool qInsideTvS : TyVarIdS qOrphanTvS : TyVarIdS visit 1: inherited attributes: baseQu : TyQu defaultedVarMp : VarMp fxTvM : TvCatMp isRow : Bool qSurrTvS : TyVarIdS rank : Int tvIsBound : TvLevIsBound tyCtxt : TyQuCtxt synthesized attributes: quTy : Ty self : Ty alternatives: alternative Con: child nm : {HsName} visit 0: local frTvS : _ visit 1: local quTy : _ local self : _ alternative App: child func : Ty child arg : Ty visit 0: local isAtTop : _ local appFunNm : {HsName} local isSpineRoot : {Bool} local appIsSum : _ local appIsRec : {Bool} local appIsRecOrSum : _ local argIsRow : {Bool} local appIsArrow : {Bool} local isArrowArg : {Bool} local isArrowRoot : {Bool} local appIsLikeProd : {Bool} local polArrowRes : _ local _tup1 : _ local frTvSL : {[TyVarIdS]} local frRowTvS : {TyVarIdS} local frTvS : {TyVarIdS} local isQuLocExtraHook : _ local isProdRoot : _ local isQuLoc : {Bool} local qOrphanTvS : {TyVarIdS} local qHereTvS : {TyVarIdS} visit 1: local tyCtxt : _ local qAsExist : _ local hereQu : _ local isQuFxLoc : _ local _tup3 : _ local tvIsBound : _ local defaultedVarMpNew : _ local defaultedVarMp : _ local qSurrTvS : _ local quTyBase : _ local qBndL1Tvs : _ local qBndExTvs : _ local qBndTvs : _ local isQuRank : _ local self : _ intra appIsLikeProd : {Bool} intra appIsArrow : {Bool} intra qHereTvS : {TyVarIdS} intra isQuLoc : {Bool} intra isArrowArg : {Bool} intra argIsRow : {Bool} intra frRowTvS : {TyVarIdS} alternative Ann: child ann : TyAnn child ty : Ty visit 0: local isAtTop : _ visit 1: local tyCtxt : _ local isRow : _ local quTy : _ local self : _ alternative Dbg: child info : {String} visit 1: local quTy : _ local self : _ alternative Any: visit 0: local frTvS : _ visit 1: local quTy : _ local self : _ alternative Var: child tv : {TyVarId} child categ : TyVarCateg visit 0: local frTvS : {TyVarIdS} local isQuLocExtraHook : _ local isQuLoc : {Bool} visit 1: local quTyBase : _ local qAsExist : _ local hereQu : _ local isQuFxLoc : _ local qHereTvS : _ local _tup5 : _ local qBndL1Tvs : _ local qBndExTvs : _ local qBndTvs : _ local isQuRank : _ local self : _ intra frTvS : {TyVarIdS} intra isQuLoc : {Bool} alternative TBind: child qu : TyQu child tv : {TyVarId} child l1 : {Ty} child ty : Ty visit 0: local introTVarS : {TyVarIdS} local isAtTop : _ local frTvS : {TyVarIdS} local isQuLocExtraHook : _ local isQuLoc : {Bool} visit 1: local tyCtxt : _ local hereQu : _ local _tup7 : _ local tvIsBoundQu : _ local isQuFxLoc : _ local qHereTvS : _ local _tup6 : _ local tvIsBound : _ local defaultedVarMpNew : _ local defaultedVarMp : _ local qSurrTvS : _ local isRow : _ local quTyBase : _ local qBndL1TvsQu : _ local qBndL1TvsOther : _ local qBndL1Tvs : _ local qBndExTvs : _ local qBndTvs : _ local isQuRank : _ local self : _ intra introTVarS : {TyVarIdS} intra frTvS : {TyVarIdS} intra isQuLoc : {Bool} alternative Ext: child ty : Ty child nm : {HsName} child extTy : Ty visit 0: local isAtTop : _ local appFunNm : {HsName} local frTvSL : _ local qOrphanTvS : _ visit 1: local tyCtxt : _ local isRow : _ local quTy : _ local self : _ alternative Pred: child pr : Pred visit 0: local isAtTop : _ local frTvS : {TyVarIdS} local isQuLocExtraHook : _ local isQuLoc : {Bool} visit 1: local tyCtxt : _ local qHereTvS : _ local _tup8 : _ local tvIsBound : _ local defaultedVarMpNew : _ local defaultedVarMp : _ local qAsExist : _ local hereQu : _ local qBndL1Tvs : _ local qBndExTvs : _ local qBndTvs : _ local isQuRank : _ local isRow : _ local self : _ intra frTvS : {TyVarIdS} intra isQuLoc : {Bool} alternative Lam: child tv : {TyVarId} child ty : Ty visit 0: local introTVarS : {TyVarIdS} local isAtTop : _ local frTvS : _ visit 1: local tyCtxt : _ local tvIsBound : _ local isRow : _ local self : _ intra introTVarS : {TyVarIdS} alternative Impls: child impls : Impls visit 0: local isAtTop : _ local frTvS : _ visit 1: local tyCtxt : _ local isRow : _ local quTy : _ local self : _ -} -- cata sem_Ty :: Ty -> T_Ty sem_Ty (Ty_Con _nm) = (sem_Ty_Con _nm) sem_Ty (Ty_App _func _arg) = (sem_Ty_App (sem_Ty _func) (sem_Ty _arg)) sem_Ty (Ty_Ann _ann _ty) = (sem_Ty_Ann (sem_TyAnn _ann) (sem_Ty _ty)) sem_Ty (Ty_Dbg _info) = (sem_Ty_Dbg _info) sem_Ty (Ty_Any) = (sem_Ty_Any) sem_Ty (Ty_Var _tv _categ) = (sem_Ty_Var _tv (sem_TyVarCateg _categ)) sem_Ty (Ty_TBind _qu _tv _l1 _ty) = (sem_Ty_TBind (sem_TyQu _qu) _tv _l1 (sem_Ty _ty)) sem_Ty (Ty_Ext _ty _nm _extTy) = (sem_Ty_Ext (sem_Ty _ty) _nm (sem_Ty _extTy)) sem_Ty (Ty_Pred _pr) = (sem_Ty_Pred (sem_Pred _pr)) sem_Ty (Ty_Lam _tv _ty) = (sem_Ty_Lam _tv (sem_Ty _ty)) sem_Ty (Ty_Impls _impls) = (sem_Ty_Impls (sem_Impls _impls)) -- semantic domain type T_Ty = Int -> Bool -> TyQuOpts -> Polarity -> ( HsName,([TyVarIdS]),TvCatMp,Bool,Bool,Bool,TyVarIdS,TyVarIdS,T_Ty_1) type T_Ty_1 = TyQu -> VarMp -> TvCatMp -> Bool -> TyVarIdS -> Int -> TvLevIsBound -> TyQuCtxt -> ( Ty,Ty) sem_Ty_Con :: HsName -> T_Ty sem_Ty_Con nm_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (nm_) of { _lhsOappFunNm -> (case (Set.empty) of { _frTvS -> (case ([_frTvS]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (False) of { _lhsOisQuLoc -> (case (Set.empty) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Con_1 :: T_Ty_1 sem_Ty_Con_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (Ty_Con nm_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Ty_Con nm_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_Ty_Con_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) })) sem_Ty_App :: T_Ty -> T_Ty -> T_Ty sem_Ty_App func_ arg_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (_lhsIopts) of { _funcOopts -> (case (False) of { _isAtTop -> (case (_isAtTop) of { _funcOisAtTop -> (case (_lhsIappSpinePos + 1) of { _funcOappSpinePos -> (case (_lhsIpol) of { _funcOpol -> (case (func_ _funcOappSpinePos _funcOisAtTop _funcOopts _funcOpol) of { ( _funcIappFunNm,_funcIfrTvSL,_funcIgathFxTvM,_funcIisArrow,_funcIisPred,_funcIisQuLoc,_funcIqInsideTvS,_funcIqOrphanTvS,func_1) -> (case (_funcIappFunNm) of { _appFunNm -> (case (_appFunNm) of { _lhsOappFunNm -> (case (_lhsIappSpinePos == 0) of { _isSpineRoot -> (case (0) of { _argOappSpinePos -> (case (hsnIsSum _funcIappFunNm) of { _appIsSum -> (case (hsnIsRec _funcIappFunNm) of { _appIsRec -> (case (_appIsRec || _appIsSum) of { _appIsRecOrSum -> (case (_isSpineRoot && _appIsRecOrSum) of { _argIsRow -> (case (_lhsIopts) of { _argOopts -> (case (_isAtTop) of { _argOisAtTop -> (case (hsnIsArrow _funcIappFunNm) of { _appIsArrow -> (case (_appIsArrow && _lhsIappSpinePos == 1) of { _isArrowArg -> (case (_appIsArrow && _isSpineRoot) of { _isArrowRoot -> (case (hsnIsProd _funcIappFunNm || _appIsRec) of { _appIsLikeProd -> (case (if _funcIisPred then _lhsIpol else polCovariant) of { _polArrowRes -> (case (if _appIsLikeProd then _lhsIpol else if _isArrowRoot then _polArrowRes else if _isArrowArg then polContravariant else polInvariant) of { _argOpol -> (case (arg_ _argOappSpinePos _argOisAtTop _argOopts _argOpol) of { ( _argIappFunNm,_argIfrTvSL,_argIgathFxTvM,_argIisArrow,_argIisPred,_argIisQuLoc,_argIqInsideTvS,_argIqOrphanTvS,arg_1) -> (case (if _argIsRow then hdAndTl (reverse _argIfrTvSL) else (Set.empty,_argIfrTvSL ++ _funcIfrTvSL)) of { __tup1 -> (case (__tup1) of { (_,_frTvSL) -> (case (__tup1) of { (_frRowTvS,_) -> (case (Set.unions (_frRowTvS : _frTvSL)) of { _frTvS -> (case (if _isSpineRoot then [_frTvS] else _frTvSL) of { _lhsOfrTvSL -> (case (_funcIgathFxTvM `Map.union` _argIgathFxTvM) of { _lhsOgathFxTvM -> (case (_isArrowRoot) of { _lhsOisArrow -> (case (if _isArrowArg then _argIisPred else False) of { _lhsOisPred -> (case (_lhsIisAtTop || tqoptAllowInnerQuant _lhsIopts) of { _isQuLocExtraHook -> (case (_appIsLikeProd && _isSpineRoot) of { _isProdRoot -> (case (( polIsCovariant _lhsIpol || (polIsContravariant _lhsIpol && (_isProdRoot || _isArrowRoot && (not _funcIisPred || _argIisQuLoc) ) ) ) && _isQuLocExtraHook) of { _isQuLoc -> (case (if _isArrowArg then _argIisQuLoc else _isQuLoc) of { _lhsOisQuLoc -> (case (_argIqOrphanTvS `Set.union` _funcIqOrphanTvS) of { _qOrphanTvS -> (case (if _isQuLoc then if _appIsArrow || _appIsLikeProd then Set.unions [tvarSOccurGE2 _frTvSL, _frRowTvS, _qOrphanTvS] else _frTvS else Set.empty) of { _qHereTvS -> (case (_qHereTvS) of { _lhsOqInsideTvS -> (case (if _isSpineRoot && _isQuLoc then Set.empty else _qOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_App_1 :: T_Ty_1 sem_Ty_App_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (if _appIsArrow then TyQuCtxtArrow else if _appIsLikeProd then TyQuCtxtProd else TyQuCtxtOther) of { _tyCtxt -> (case (_tyCtxt) of { _argOtyCtxt -> (case ((_appIsLikeProd || polIsContravariant _lhsIpol && not _appIsArrow)) of { _qAsExist -> (case (if _qAsExist then tyquExists _lhsIbaseQu else _lhsIbaseQu) of { _hereQu -> (case (_lhsIrank > 1 || _lhsIrank == 1 && (_lhsItyCtxt == TyQuCtxtArrow && not _argIisArrow || _lhsItyCtxt == TyQuCtxtOther )) of { _isQuFxLoc -> (case (tvarsToQuant _lhsIopts _isQuLoc _lhsIfxTvM (tvMayQuFx _hereQu _lhsIfxTvM _isQuFxLoc) _lhsItvIsBound _qHereTvS) of { __tup3 -> (case (__tup3) of { (_,_,_,_tvIsBound,_) -> (case (_tvIsBound) of { _argOtvIsBound -> (case (_lhsIfxTvM) of { _argOfxTvM -> (case (__tup3) of { (_,_,_,_,_defaultedVarMpNew) -> (case (_defaultedVarMpNew `varUpd` _lhsIdefaultedVarMp) of { _defaultedVarMp -> (case (_defaultedVarMp) of { _argOdefaultedVarMp -> (case (_lhsIbaseQu) of { _argObaseQu -> (case (_tyCtxt) of { _funcOtyCtxt -> (case (_tvIsBound) of { _funcOtvIsBound -> (case (_lhsIrank) of { _funcOrank -> (case (_lhsIfxTvM) of { _funcOfxTvM -> (case (_defaultedVarMp) of { _funcOdefaultedVarMp -> (case (_lhsIbaseQu) of { _funcObaseQu -> (case (_lhsIrank + (if _isArrowArg then 1 else 0)) of { _argOrank -> (case (_qHereTvS `Set.union` _lhsIqSurrTvS) of { _qSurrTvS -> (case (_qSurrTvS) of { _argOqSurrTvS -> (case (_argIsRow) of { _argOisRow -> (case (arg_1 _argObaseQu _argOdefaultedVarMp _argOfxTvM _argOisRow _argOqSurrTvS _argOrank _argOtvIsBound _argOtyCtxt) of { ( _argIquTy,_argIself) -> (case (_qSurrTvS) of { _funcOqSurrTvS -> (case (_lhsIisRow) of { _funcOisRow -> (case (func_1 _funcObaseQu _funcOdefaultedVarMp _funcOfxTvM _funcOisRow _funcOqSurrTvS _funcOrank _funcOtvIsBound _funcOtyCtxt) of { ( _funcIquTy,_funcIself) -> (case (Ty_App _funcIquTy _argIquTy) of { _quTyBase -> (case (__tup3) of { (_,_,_qBndL1Tvs,_,_) -> (case (__tup3) of { (_,_qBndExTvs,_,_,_) -> (case (__tup3) of { (_qBndTvs,_,_,_,_) -> (case (_lhsIrank `elem` tqoptQuRanks _lhsIopts) of { _isQuRank -> (case (let (rwYTvS,rwNTvS) = partition (\(v,_) -> v `Set.member` _frRowTvS) _qBndTvs in mkTyQuForRank _lhsIopts _isQuRank _hereQu _qBndL1Tvs rwNTvS _qBndExTvs $ mkTyQuForRank _lhsIopts _isQuRank _lhsIbaseQu [] rwYTvS [] $ _quTyBase) of { _lhsOquTy -> (case (Ty_App _funcIself _argIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_App_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Ty_Ann :: T_TyAnn -> T_Ty -> T_Ty sem_Ty_Ann ann_ ty_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case (_lhsIappSpinePos) of { _tyOappSpinePos -> (case (_lhsIpol) of { _tyOpol -> (case (_lhsIopts) of { _tyOopts -> (case (False) of { _isAtTop -> (case (_isAtTop) of { _tyOisAtTop -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (_tyIfrTvSL) of { _lhsOfrTvSL -> (case (_tyIgathFxTvM) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (_tyIisQuLoc) of { _lhsOisQuLoc -> (case (_tyIqInsideTvS) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Ann_1 :: T_Ty_1 sem_Ty_Ann_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (TyQuCtxtOther) of { _tyCtxt -> (case (_tyCtxt) of { _tyOtyCtxt -> (case (_lhsItvIsBound) of { _tyOtvIsBound -> (case (_lhsIrank) of { _tyOrank -> (case (_lhsIfxTvM) of { _tyOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (_lhsIqSurrTvS) of { _tyOqSurrTvS -> (case (False) of { _isRow -> (case (_isRow) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (ann_) of { ( _annIquTy,_annIself) -> (case (Ty_Ann _annIquTy _tyIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Ty_Ann _annIself _tyIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_Ann_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Ty_Dbg :: String -> T_Ty sem_Ty_Dbg info_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case ([]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (False) of { _lhsOisQuLoc -> (case (Set.empty) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Dbg_1 :: T_Ty_1 sem_Ty_Dbg_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (Ty_Dbg info_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Ty_Dbg info_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_Ty_Dbg_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) })) sem_Ty_Any :: T_Ty sem_Ty_Any = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case (Set.empty) of { _frTvS -> (case ([_frTvS]) of { _lhsOfrTvSL -> (case (Map.empty) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (False) of { _lhsOisQuLoc -> (case (Set.empty) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Any_1 :: T_Ty_1 sem_Ty_Any_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (Ty_Any) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Ty_Any) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })) in sem_Ty_Any_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) })) sem_Ty_Var :: TyVarId -> T_TyVarCateg -> T_Ty sem_Ty_Var tv_ categ_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case (categ_) of { ( _categIquTy,_categIself) -> (case (if tvCatIsPlain _categIself then Set.singleton tv_ else Set.empty) of { _frTvS -> (case ([_frTvS]) of { _lhsOfrTvSL -> (case (tv_ `Map.singleton` mkTvInfoTy _categIself) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (_lhsIisAtTop || tqoptAllowInnerQuant _lhsIopts) of { _isQuLocExtraHook -> (case (polIsCovariant _lhsIpol && _isQuLocExtraHook) of { _isQuLoc -> (case (_isQuLoc) of { _lhsOisQuLoc -> (case (Set.empty) of { _lhsOqInsideTvS -> (case (if _isQuLoc then Set.empty else _frTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Var_1 :: T_Ty_1 sem_Ty_Var_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (maybe (Ty_Var tv_ _categIquTy) id $ varmpTyLookup tv_ _lhsIdefaultedVarMp) of { _quTyBase -> (case (polIsContravariant _lhsIpol) of { _qAsExist -> (case (if _qAsExist then tyquExists _lhsIbaseQu else _lhsIbaseQu) of { _hereQu -> (case (False) of { _isQuFxLoc -> (case (if _isQuLoc then _frTvS else Set.empty) of { _qHereTvS -> (case (tvarsToQuant _lhsIopts _isQuLoc _lhsIfxTvM (tvMayQuFx _hereQu _lhsIfxTvM _isQuFxLoc) _lhsItvIsBound _qHereTvS) of { __tup5 -> (case (__tup5) of { (_,_,_qBndL1Tvs,_,_) -> (case (__tup5) of { (_,_qBndExTvs,_,_,_) -> (case (__tup5) of { (_qBndTvs,_,_,_,_) -> (case (_lhsIrank `elem` tqoptQuRanks _lhsIopts) of { _isQuRank -> (case (mkTyQuForRank _lhsIopts _isQuRank _hereQu _qBndL1Tvs _qBndTvs _qBndExTvs _quTyBase) of { _lhsOquTy -> (case (Ty_Var tv_ _categIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_Var_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Ty_TBind :: T_TyQu -> TyVarId -> Ty -> T_Ty -> T_Ty sem_Ty_TBind qu_ tv_ l1_ ty_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case (Set.singleton tv_) of { _introTVarS -> (case (0) of { _tyOappSpinePos -> (case (_lhsIpol) of { _tyOpol -> (case (_lhsIopts) of { _tyOopts -> (case (False) of { _isAtTop -> (case (_isAtTop) of { _tyOisAtTop -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (head _tyIfrTvSL `Set.difference` _introTVarS) of { _frTvS -> (case ([_frTvS]) of { _lhsOfrTvSL -> (case (_tyIgathFxTvM) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (_lhsIisAtTop || tqoptAllowInnerQuant _lhsIopts) of { _isQuLocExtraHook -> (case (not (polIsInvariant _lhsIpol) && _isQuLocExtraHook) of { _isQuLoc -> (case (_isQuLoc) of { _lhsOisQuLoc -> (case (_tyIqInsideTvS) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_TBind_1 :: T_Ty_1 sem_Ty_TBind_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (TyQuCtxtOther) of { _tyCtxt -> (case (_tyCtxt) of { _tyOtyCtxt -> (case (tyQu_Forall) of { _hereQu -> (case (let (qBndL1Tvs,_,isB) = tvarsToQuantL1 [(tv_,l1_)] _lhsItvIsBound in (qBndL1Tvs, tvBoundAddS 0 _introTVarS isB)) of { __tup7 -> (case (__tup7) of { (_,_tvIsBoundQu) -> (case (False) of { _isQuFxLoc -> (case (if _isQuLoc then _frTvS else Set.empty) of { _qHereTvS -> (case (tvarsToQuant _lhsIopts _isQuLoc _lhsIfxTvM (tvMayQuFx _hereQu _lhsIfxTvM _isQuFxLoc) _tvIsBoundQu _qHereTvS) of { __tup6 -> (case (__tup6) of { (_,_,_,_tvIsBound,_) -> (case (_tvIsBound) of { _tyOtvIsBound -> (case (_lhsIrank) of { _tyOrank -> (case (_lhsIfxTvM) of { _tyOfxTvM -> (case (__tup6) of { (_,_,_,_,_defaultedVarMpNew) -> (case (_defaultedVarMpNew `varUpd` _lhsIdefaultedVarMp) of { _defaultedVarMp -> (case (_defaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (_qHereTvS `Set.union` _lhsIqSurrTvS) of { _qSurrTvS -> (case (_qSurrTvS) of { _tyOqSurrTvS -> (case (False) of { _isRow -> (case (_isRow) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (qu_) of { ( _quIquTy,_quIself) -> (case (Ty_TBind _quIself tv_ l1_ _tyIquTy) of { _quTyBase -> (case (__tup7) of { (_qBndL1TvsQu,_) -> (case (__tup6) of { (_,_,_qBndL1TvsOther,_,_) -> (case (_qBndL1TvsOther ++ _qBndL1TvsQu) of { _qBndL1Tvs -> (case (__tup6) of { (_,_qBndExTvs,_,_,_) -> (case (__tup6) of { (_qBndTvs,_,_,_,_) -> (case (_lhsIrank `elem` tqoptQuRanks _lhsIopts) of { _isQuRank -> (case (mkTyQuForRank _lhsIopts _isQuRank _hereQu _qBndL1Tvs _qBndTvs _qBndExTvs _quTyBase) of { _lhsOquTy -> (case (Ty_TBind _quIself tv_ l1_ _tyIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_TBind_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Ty_Ext :: T_Ty -> HsName -> T_Ty -> T_Ty sem_Ty_Ext ty_ nm_ extTy_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (_lhsIpol) of { _tyOpol -> (case (_lhsIopts) of { _tyOopts -> (case (False) of { _isAtTop -> (case (_isAtTop) of { _tyOisAtTop -> (case (_lhsIappSpinePos + 1) of { _tyOappSpinePos -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (_tyIappFunNm) of { _appFunNm -> (case (_appFunNm) of { _lhsOappFunNm -> (case (0) of { _extTyOappSpinePos -> (case (_lhsIpol) of { _extTyOpol -> (case (_lhsIopts) of { _extTyOopts -> (case (_isAtTop) of { _extTyOisAtTop -> (case (extTy_ _extTyOappSpinePos _extTyOisAtTop _extTyOopts _extTyOpol) of { ( _extTyIappFunNm,_extTyIfrTvSL,_extTyIgathFxTvM,_extTyIisArrow,_extTyIisPred,_extTyIisQuLoc,_extTyIqInsideTvS,_extTyIqOrphanTvS,extTy_1) -> (case (_extTyIfrTvSL ++ _tyIfrTvSL) of { _frTvSL -> (case (_frTvSL) of { _lhsOfrTvSL -> (case (_tyIgathFxTvM `Map.union` _extTyIgathFxTvM) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (_tyIisQuLoc && _extTyIisQuLoc) of { _lhsOisQuLoc -> (case (_tyIqInsideTvS `Set.union` _extTyIqInsideTvS) of { _lhsOqInsideTvS -> (case (_extTyIqOrphanTvS `Set.union` _tyIqOrphanTvS) of { _qOrphanTvS -> (case (_qOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Ext_1 :: T_Ty_1 sem_Ty_Ext_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (TyQuCtxtOther) of { _tyCtxt -> (case (_tyCtxt) of { _extTyOtyCtxt -> (case (_lhsItvIsBound) of { _extTyOtvIsBound -> (case (_lhsIrank) of { _extTyOrank -> (case (_lhsIfxTvM) of { _extTyOfxTvM -> (case (_lhsIdefaultedVarMp) of { _extTyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _extTyObaseQu -> (case (_tyCtxt) of { _tyOtyCtxt -> (case (_lhsItvIsBound) of { _tyOtvIsBound -> (case (_lhsIrank) of { _tyOrank -> (case (_lhsIfxTvM) of { _tyOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (_lhsIqSurrTvS) of { _extTyOqSurrTvS -> (case (False) of { _isRow -> (case (_isRow) of { _extTyOisRow -> (case (extTy_1 _extTyObaseQu _extTyOdefaultedVarMp _extTyOfxTvM _extTyOisRow _extTyOqSurrTvS _extTyOrank _extTyOtvIsBound _extTyOtyCtxt) of { ( _extTyIquTy,_extTyIself) -> (case (_lhsIqSurrTvS) of { _tyOqSurrTvS -> (case (_isRow) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (Ty_Ext _tyIquTy nm_ _extTyIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Ty_Ext _tyIself nm_ _extTyIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_Ext_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Ty_Pred :: T_Pred -> T_Ty sem_Ty_Pred pr_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case (_lhsIopts) of { _prOopts -> (case (False) of { _isAtTop -> (case (_isAtTop) of { _prOisAtTop -> (case (polInvariant) of { _prOpol -> (case (pr_ _prOisAtTop _prOopts _prOpol) of { ( _prIfrTvSL,_prIgathFxTvM,_prIqInsideTvS,_prIqOrphanTvS,pr_1) -> (case (Set.unions _prIfrTvSL) of { _frTvS -> (case ([_frTvS]) of { _lhsOfrTvSL -> (case (_prIgathFxTvM) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (True) of { _lhsOisPred -> (case (_lhsIisAtTop || tqoptAllowInnerQuant _lhsIopts) of { _isQuLocExtraHook -> (case (polIsCovariant _lhsIpol && _isQuLocExtraHook) of { _isQuLoc -> (case (_isQuLoc) of { _lhsOisQuLoc -> (case (_prIqInsideTvS) of { _lhsOqInsideTvS -> (case (_prIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Pred_1 :: T_Ty_1 sem_Ty_Pred_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (TyQuCtxtOther) of { _tyCtxt -> (case (_tyCtxt) of { _prOtyCtxt -> (case (_frTvS `Set.difference` _prIqInsideTvS) of { _qHereTvS -> (case (tvarsToQuant _lhsIopts _isQuLoc _lhsIfxTvM (const False) _lhsItvIsBound _qHereTvS) of { __tup8 -> (case (__tup8) of { (_,_,_,_tvIsBound,_) -> (case (_tvIsBound) of { _prOtvIsBound -> (case (_lhsIrank) of { _prOrank -> (case (_lhsIfxTvM) of { _prOfxTvM -> (case (__tup8) of { (_,_,_,_,_defaultedVarMpNew) -> (case (_defaultedVarMpNew `varUpd` _lhsIdefaultedVarMp) of { _defaultedVarMp -> (case (_defaultedVarMp) of { _prOdefaultedVarMp -> (case (_lhsIbaseQu) of { _prObaseQu -> (case (polIsContravariant _lhsIpol) of { _qAsExist -> (case (if _qAsExist then tyquExists _lhsIbaseQu else _lhsIbaseQu) of { _hereQu -> (case (__tup8) of { (_,_,_qBndL1Tvs,_,_) -> (case (__tup8) of { (_,_qBndExTvs,_,_,_) -> (case (__tup8) of { (_qBndTvs,_,_,_,_) -> (case (_lhsIrank `elem` tqoptQuRanks _lhsIopts) of { _isQuRank -> (case (_lhsIqSurrTvS) of { _prOqSurrTvS -> (case (False) of { _isRow -> (case (_isRow) of { _prOisRow -> (case (pr_1 _prObaseQu _prOdefaultedVarMp _prOfxTvM _prOisRow _prOqSurrTvS _prOrank _prOtvIsBound _prOtyCtxt) of { ( _prIquTy,_prIself) -> (case (mkTyQuForRank _lhsIopts _isQuRank _hereQu _qBndL1Tvs _qBndTvs _qBndExTvs (mkTyPr _prIquTy)) of { _lhsOquTy -> (case (Ty_Pred _prIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_Pred_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Ty_Lam :: TyVarId -> T_Ty -> T_Ty sem_Ty_Lam tv_ ty_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case (_lhsIappSpinePos) of { _tyOappSpinePos -> (case (Set.singleton tv_) of { _introTVarS -> (case (_lhsIpol) of { _tyOpol -> (case (_lhsIopts) of { _tyOopts -> (case (False) of { _isAtTop -> (case (_isAtTop) of { _tyOisAtTop -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (head _tyIfrTvSL `Set.difference` _introTVarS) of { _frTvS -> (case ([_frTvS]) of { _lhsOfrTvSL -> (case (_tyIgathFxTvM) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (False) of { _lhsOisPred -> (case (_tyIisQuLoc) of { _lhsOisQuLoc -> (case (_tyIqInsideTvS) of { _lhsOqInsideTvS -> (case (Set.empty) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Lam_1 :: T_Ty_1 sem_Ty_Lam_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (TyQuCtxtOther) of { _tyCtxt -> (case (_tyCtxt) of { _tyOtyCtxt -> (case (tvBoundAddS 0 _introTVarS _lhsItvIsBound) of { _tvIsBound -> (case (_tvIsBound) of { _tyOtvIsBound -> (case (_lhsIrank) of { _tyOrank -> (case (_lhsIfxTvM) of { _tyOfxTvM -> (case (_lhsIdefaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (_lhsIqSurrTvS) of { _tyOqSurrTvS -> (case (False) of { _isRow -> (case (_isRow) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (Ty_Lam tv_ _tyIquTy) of { _lhsOquTy -> (case (Ty_Lam tv_ _tyIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_Lam_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) sem_Ty_Impls :: T_Impls -> T_Ty sem_Ty_Impls impls_ = (\ _lhsIappSpinePos _lhsIisAtTop _lhsIopts _lhsIpol -> (case (hsnUnknown) of { _lhsOappFunNm -> (case (_lhsIpol) of { _implsOpol -> (case (_lhsIopts) of { _implsOopts -> (case (False) of { _isAtTop -> (case (_isAtTop) of { _implsOisAtTop -> (case (impls_ _implsOisAtTop _implsOopts _implsOpol) of { ( _implsIfrTvSL,_implsIgathFxTvM,_implsIqInsideTvS,_implsIqOrphanTvS,impls_1) -> (case (Set.unions _implsIfrTvSL) of { _frTvS -> (case ([_frTvS]) of { _lhsOfrTvSL -> (case (_implsIgathFxTvM) of { _lhsOgathFxTvM -> (case (False) of { _lhsOisArrow -> (case (True) of { _lhsOisPred -> (case (False) of { _lhsOisQuLoc -> (case (_implsIqInsideTvS) of { _lhsOqInsideTvS -> (case (_implsIqOrphanTvS) of { _lhsOqOrphanTvS -> (case ((let sem_Ty_Impls_1 :: T_Ty_1 sem_Ty_Impls_1 = (\ _lhsIbaseQu _lhsIdefaultedVarMp _lhsIfxTvM _lhsIisRow _lhsIqSurrTvS _lhsIrank _lhsItvIsBound _lhsItyCtxt -> (case (TyQuCtxtOther) of { _tyCtxt -> (case (_tyCtxt) of { _implsOtyCtxt -> (case (_lhsItvIsBound) of { _implsOtvIsBound -> (case (_lhsIrank) of { _implsOrank -> (case (_lhsIfxTvM) of { _implsOfxTvM -> (case (_lhsIdefaultedVarMp) of { _implsOdefaultedVarMp -> (case (_lhsIbaseQu) of { _implsObaseQu -> (case (_lhsIqSurrTvS) of { _implsOqSurrTvS -> (case (False) of { _isRow -> (case (_isRow) of { _implsOisRow -> (case (impls_1 _implsObaseQu _implsOdefaultedVarMp _implsOfxTvM _implsOisRow _implsOqSurrTvS _implsOrank _implsOtvIsBound _implsOtyCtxt) of { ( _implsIquTy,_implsIself) -> (case (Ty_Impls _implsIquTy) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (Ty_Impls _implsIself) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) in sem_Ty_Impls_1)) of { ( sem_Ty_1) -> ( _lhsOappFunNm,_lhsOfrTvSL,_lhsOgathFxTvM,_lhsOisArrow,_lhsOisPred,_lhsOisQuLoc,_lhsOqInsideTvS,_lhsOqOrphanTvS,sem_Ty_1) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) -- TyAGItf ----------------------------------------------------- {- visit 0: inherited attributes: baseQu : TyQu opts : TyQuOpts synthesized attribute: quTy : Ty alternatives: alternative AGItf: child ty : Ty visit 0: local opts : _ local fxTvM : _ local qHereTvS : _ local _tup9 : _ local tvIsBound : _ local rank : _ local defaultedVarMpNew : _ local defaultedVarMp : _ local qSurrTvS : _ local quTyBase : _ local hereQu : _ local qBndL1Tvs : _ local qBndExTvs : _ local qBndTvs : _ local isQuRank : _ -} -- cata sem_TyAGItf :: TyAGItf -> T_TyAGItf sem_TyAGItf (TyAGItf_AGItf _ty) = (sem_TyAGItf_AGItf (sem_Ty _ty)) -- semantic domain type T_TyAGItf = TyQu -> TyQuOpts -> ( Ty) data Inh_TyAGItf = Inh_TyAGItf {baseQu_Inh_TyAGItf :: !(TyQu),opts_Inh_TyAGItf :: !(TyQuOpts)} data Syn_TyAGItf = Syn_TyAGItf {quTy_Syn_TyAGItf :: !(Ty)} wrap_TyAGItf :: T_TyAGItf -> Inh_TyAGItf -> Syn_TyAGItf wrap_TyAGItf sem (Inh_TyAGItf _lhsIbaseQu _lhsIopts) = (let ( _lhsOquTy) = sem _lhsIbaseQu _lhsIopts in (Syn_TyAGItf _lhsOquTy)) sem_TyAGItf_AGItf :: T_Ty -> T_TyAGItf sem_TyAGItf_AGItf ty_ = (\ _lhsIbaseQu _lhsIopts -> (case (_lhsIopts { tqoptQuRanks = take 5 (tqoptQuRanks _lhsIopts) }) of { _opts -> (case (_opts) of { _tyOopts -> (case (polCovariant) of { _tyOpol -> (case (0) of { _tyOappSpinePos -> (case (True) of { _tyOisAtTop -> (case (ty_ _tyOappSpinePos _tyOisAtTop _tyOopts _tyOpol) of { ( _tyIappFunNm,_tyIfrTvSL,_tyIgathFxTvM,_tyIisArrow,_tyIisPred,_tyIisQuLoc,_tyIqInsideTvS,_tyIqOrphanTvS,ty_1) -> (case (_tyIgathFxTvM) of { _fxTvM -> (case (Set.empty) of { _qHereTvS -> (case (tvarsToQuant _lhsIopts True _fxTvM (const False) (tvIsBound2L0 $ tqoptTvIsBound _lhsIopts) _qHereTvS) of { __tup9 -> (case (__tup9) of { (_,_,_,_tvIsBound,_) -> (case (_tvIsBound) of { _tyOtvIsBound -> (case (1) of { _rank -> (case (_rank) of { _tyOrank -> (case (_fxTvM) of { _tyOfxTvM -> (case (__tup9) of { (_,_,_,_,_defaultedVarMpNew) -> (case (_defaultedVarMpNew) of { _defaultedVarMp -> (case (_defaultedVarMp) of { _tyOdefaultedVarMp -> (case (_lhsIbaseQu) of { _tyObaseQu -> (case (TyQuCtxtOnTop) of { _tyOtyCtxt -> (case (_qHereTvS) of { _qSurrTvS -> (case (_qSurrTvS) of { _tyOqSurrTvS -> (case (False) of { _tyOisRow -> (case (ty_1 _tyObaseQu _tyOdefaultedVarMp _tyOfxTvM _tyOisRow _tyOqSurrTvS _tyOrank _tyOtvIsBound _tyOtyCtxt) of { ( _tyIquTy,_tyIself) -> (case (_tyIquTy) of { _quTyBase -> (case (_lhsIbaseQu) of { _hereQu -> (case (__tup9) of { (_,_,_qBndL1Tvs,_,_) -> (case (__tup9) of { (_,_qBndExTvs,_,_,_) -> (case (__tup9) of { (_qBndTvs,_,_,_,_) -> (case (_rank `elem` tqoptQuRanks _opts) of { _isQuRank -> (case (mkTyQuForRank _lhsIopts _isQuRank _hereQu _qBndL1Tvs _qBndTvs _qBndExTvs _quTyBase) of { _lhsOquTy -> ( _lhsOquTy) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) }) })) -- TyAnn ------------------------------------------------------- {- visit 0: synthesized attributes: quTy : TyAnn self : TyAnn alternatives: alternative Empty: visit 0: local quTy : _ local self : _ alternative Strictness: child s : {Strictness} visit 0: local quTy : _ local self : _ alternative Mono: visit 0: local quTy : _ local self : _ -} -- cata sem_TyAnn :: TyAnn -> T_TyAnn sem_TyAnn (TyAnn_Empty) = (sem_TyAnn_Empty) sem_TyAnn (TyAnn_Strictness _s) = (sem_TyAnn_Strictness _s) sem_TyAnn (TyAnn_Mono) = (sem_TyAnn_Mono) -- semantic domain type T_TyAnn = ( TyAnn,TyAnn) sem_TyAnn_Empty :: T_TyAnn sem_TyAnn_Empty = (case (TyAnn_Empty) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyAnn_Empty) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) sem_TyAnn_Strictness :: Strictness -> T_TyAnn sem_TyAnn_Strictness s_ = (case (TyAnn_Strictness s_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyAnn_Strictness s_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) sem_TyAnn_Mono :: T_TyAnn sem_TyAnn_Mono = (case (TyAnn_Mono) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyAnn_Mono) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) -- TyQu -------------------------------------------------------- {- visit 0: synthesized attributes: quTy : TyQu self : TyQu alternatives: alternative Forall: child mlev : {MetaLev} visit 0: local quTy : _ local self : _ alternative Exists: child mlev : {MetaLev} visit 0: local quTy : _ local self : _ alternative Plain: child mlev : {MetaLev} visit 0: local quTy : _ local self : _ -} -- cata sem_TyQu :: TyQu -> T_TyQu sem_TyQu (TyQu_Forall _mlev) = (sem_TyQu_Forall _mlev) sem_TyQu (TyQu_Exists _mlev) = (sem_TyQu_Exists _mlev) sem_TyQu (TyQu_Plain _mlev) = (sem_TyQu_Plain _mlev) -- semantic domain type T_TyQu = ( TyQu,TyQu) sem_TyQu_Forall :: MetaLev -> T_TyQu sem_TyQu_Forall mlev_ = (case (TyQu_Forall mlev_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyQu_Forall mlev_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) sem_TyQu_Exists :: MetaLev -> T_TyQu sem_TyQu_Exists mlev_ = (case (TyQu_Exists mlev_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyQu_Exists mlev_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) sem_TyQu_Plain :: MetaLev -> T_TyQu sem_TyQu_Plain mlev_ = (case (TyQu_Plain mlev_) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyQu_Plain mlev_) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) -- TyVarCateg -------------------------------------------------- {- visit 0: synthesized attributes: quTy : TyVarCateg self : TyVarCateg alternatives: alternative Plain: visit 0: local quTy : _ local self : _ alternative Fixed: visit 0: local quTy : _ local self : _ alternative Meta: visit 0: local quTy : _ local self : _ -} -- cata sem_TyVarCateg :: TyVarCateg -> T_TyVarCateg sem_TyVarCateg (TyVarCateg_Plain) = (sem_TyVarCateg_Plain) sem_TyVarCateg (TyVarCateg_Fixed) = (sem_TyVarCateg_Fixed) sem_TyVarCateg (TyVarCateg_Meta) = (sem_TyVarCateg_Meta) -- semantic domain type T_TyVarCateg = ( TyVarCateg,TyVarCateg) sem_TyVarCateg_Plain :: T_TyVarCateg sem_TyVarCateg_Plain = (case (TyVarCateg_Plain) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyVarCateg_Plain) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) sem_TyVarCateg_Fixed :: T_TyVarCateg sem_TyVarCateg_Fixed = (case (TyVarCateg_Fixed) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyVarCateg_Fixed) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) }) sem_TyVarCateg_Meta :: T_TyVarCateg sem_TyVarCateg_Meta = (case (TyVarCateg_Meta) of { _quTy -> (case (_quTy) of { _lhsOquTy -> (case (TyVarCateg_Meta) of { _self -> (case (_self) of { _lhsOself -> ( _lhsOquTy,_lhsOself) }) }) }) })