module Data.Comp.Trans.DeriveMulti ( deriveMulti ) where import Control.Lens ( _1, _2, _3, (&), (%~), (%%~), (^.), view ) import Control.Monad ( liftM ) import Control.Monad.Trans ( MonadTrans(lift) ) import Language.Haskell.TH.Syntax hiding ( lift ) import Language.Haskell.TH.ExpandSyns ( expandSyns ) import Data.Comp.Trans.Util deriveMulti :: Name -> CompTrans [Dec] deriveMulti :: Name -> CompTrans [Dec] deriveMulti Name n = do Info inf <- ReaderT TransCtx Q Info -> CompTrans Info forall a. ReaderT TransCtx Q a -> CompTrans a CompTrans (ReaderT TransCtx Q Info -> CompTrans Info) -> ReaderT TransCtx Q Info -> CompTrans Info forall a b. (a -> b) -> a -> b $ Q Info -> ReaderT TransCtx Q Info forall (m :: * -> *) a. Monad m => m a -> ReaderT TransCtx m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Q Info -> ReaderT TransCtx Q Info) -> Q Info -> ReaderT TransCtx Q Info forall a b. (a -> b) -> a -> b $ Name -> Q Info reify Name n Map Name Type substs <- Getting (Map Name Type) TransCtx (Map Name Type) -> CompTrans (Map Name Type) forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a view Getting (Map Name Type) TransCtx (Map Name Type) forall c. HasTransCtx c => Lens' c (Map Name Type) Lens' TransCtx (Map Name Type) substitutions [Name] typeArgs <- Name -> CompTrans [Name] getTypeArgs Name n if Map Name Type -> [Name] -> Bool forall a b. Ord a => Map a b -> [a] -> Bool containsAll Map Name Type substs [Name] typeArgs then case Info inf of TyConI (DataD Cxt _ Name nm [TyVarBndr BndrVis] _ Maybe Type _ [Con] cons [DerivClause] _) -> Name -> [Con] -> CompTrans [Dec] mkGADT Name nm (Map Name Type -> [Con] -> [Con] forall x. Data x => Map Name Type -> x -> x applySubsts Map Name Type substs [Con] cons) TyConI (NewtypeD Cxt _ Name nm [TyVarBndr BndrVis] _ Maybe Type _ Con con [DerivClause] _) -> Name -> [Con] -> CompTrans [Dec] mkGADT Name nm [(Map Name Type -> Con -> Con forall x. Data x => Map Name Type -> x -> x applySubsts Map Name Type substs Con con)] Info _ -> do ReaderT TransCtx Q () -> CompTrans () forall a. ReaderT TransCtx Q a -> CompTrans a CompTrans (ReaderT TransCtx Q () -> CompTrans ()) -> ReaderT TransCtx Q () -> CompTrans () forall a b. (a -> b) -> a -> b $ Q () -> ReaderT TransCtx Q () forall (m :: * -> *) a. Monad m => m a -> ReaderT TransCtx m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Q () -> ReaderT TransCtx Q ()) -> Q () -> ReaderT TransCtx Q () forall a b. (a -> b) -> a -> b $ [Char] -> Q () reportError ([Char] -> Q ()) -> [Char] -> Q () forall a b. (a -> b) -> a -> b $ [Char] "Attempted to derive multi-sorted compositional data type for " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ Name -> [Char] forall a. Show a => a -> [Char] show Name n [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ [Char] ", which is not a nullary datatype (and does not have concrete values supplied for type args)" return [] else do ReaderT TransCtx Q () -> CompTrans () forall a. ReaderT TransCtx Q a -> CompTrans a CompTrans (ReaderT TransCtx Q () -> CompTrans ()) -> ReaderT TransCtx Q () -> CompTrans () forall a b. (a -> b) -> a -> b $ Q () -> ReaderT TransCtx Q () forall (m :: * -> *) a. Monad m => m a -> ReaderT TransCtx m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Q () -> ReaderT TransCtx Q ()) -> Q () -> ReaderT TransCtx Q () forall a b. (a -> b) -> a -> b $ [Char] -> Q () reportError ([Char] -> Q ()) -> [Char] -> Q () forall a b. (a -> b) -> a -> b $ [Char] "Attempted to derive multi-sorted compositional data type for " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ Name -> [Char] forall a. Show a => a -> [Char] show Name n [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ [Char] " but it has type arguments which are not substituted away" return [] checkUniqueVar :: Con -> CompTrans () checkUniqueVar :: Con -> CompTrans () checkUniqueVar Con con = if Cxt -> Int forall a. [a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length ((Type -> Bool) -> Cxt -> Cxt forall a. (a -> Bool) -> [a] -> [a] filter Type -> Bool isVar Cxt fields) Int -> Int -> Bool forall a. Ord a => a -> a -> Bool <= Int 1 then () -> CompTrans () forall a. a -> CompTrans a forall (m :: * -> *) a. Monad m => a -> m a return () else [Char] -> CompTrans () forall a. [Char] -> CompTrans a forall (m :: * -> *) a. MonadFail m => [Char] -> m a fail ([Char] -> CompTrans ()) -> [Char] -> CompTrans () forall a b. (a -> b) -> a -> b $ [Char] "comptrans: Multiple annotion fields in constructor:" [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ Con -> [Char] forall a. Show a => a -> [Char] show Con con where fields :: [Type] fields :: Cxt fields = case Con con of RecC Name _ [VarBangType] sts -> (VarBangType -> Type) -> [VarBangType] -> Cxt forall a b. (a -> b) -> [a] -> [b] map (VarBangType -> Getting Type VarBangType Type -> Type forall s a. s -> Getting a s a -> a ^. Getting Type VarBangType Type forall s t a b. Field3 s t a b => Lens s t a b Lens VarBangType VarBangType Type Type _3) [VarBangType] sts NormalC Name _ [BangType] sts -> (BangType -> Type) -> [BangType] -> Cxt forall a b. (a -> b) -> [a] -> [b] map (BangType -> Getting Type BangType Type -> Type forall s a. s -> Getting a s a -> a ^. Getting Type BangType Type forall s t a b. Field2 s t a b => Lens s t a b Lens BangType BangType Type Type _2) [BangType] sts Con _ -> [Char] -> Cxt forall a. HasCallStack => [Char] -> a error ([Char] -> Cxt) -> [Char] -> Cxt forall a b. (a -> b) -> a -> b $ [Char] "Attempted to derive multi-sorted compositional datatype for something with non-normal constructors: " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ Con -> [Char] forall a. Show a => a -> [Char] show Con con mkGADT :: Name -> [Con] -> CompTrans [Dec] mkGADT :: Name -> [Con] -> CompTrans [Dec] mkGADT Name n [Con] cons = do Name e <- ReaderT TransCtx Q Name -> CompTrans Name forall a. ReaderT TransCtx Q a -> CompTrans a CompTrans (ReaderT TransCtx Q Name -> CompTrans Name) -> ReaderT TransCtx Q Name -> CompTrans Name forall a b. (a -> b) -> a -> b $ Q Name -> ReaderT TransCtx Q Name forall (m :: * -> *) a. Monad m => m a -> ReaderT TransCtx m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Q Name -> ReaderT TransCtx Q Name) -> Q Name -> ReaderT TransCtx Q Name forall a b. (a -> b) -> a -> b $ [Char] -> Q Name forall (m :: * -> *). Quote m => [Char] -> m Name newName [Char] "e" Name i <- ReaderT TransCtx Q Name -> CompTrans Name forall a. ReaderT TransCtx Q a -> CompTrans a CompTrans (ReaderT TransCtx Q Name -> CompTrans Name) -> ReaderT TransCtx Q Name -> CompTrans Name forall a b. (a -> b) -> a -> b $ Q Name -> ReaderT TransCtx Q Name forall (m :: * -> *) a. Monad m => m a -> ReaderT TransCtx m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Q Name -> ReaderT TransCtx Q Name) -> Q Name -> ReaderT TransCtx Q Name forall a b. (a -> b) -> a -> b $ [Char] -> Q Name forall (m :: * -> *). Quote m => [Char] -> m Name newName [Char] "i" let n' :: Name n' = Name -> Name transName Name n Maybe AnnotationPropInfo annProp <- Getting (Maybe AnnotationPropInfo) TransCtx (Maybe AnnotationPropInfo) -> CompTrans (Maybe AnnotationPropInfo) forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a view Getting (Maybe AnnotationPropInfo) TransCtx (Maybe AnnotationPropInfo) forall c. HasTransCtx c => Lens' c (Maybe AnnotationPropInfo) Lens' TransCtx (Maybe AnnotationPropInfo) annotationProp case Maybe AnnotationPropInfo annProp of Just AnnotationPropInfo _annPropInf -> (Con -> CompTrans ()) -> [Con] -> CompTrans () forall (t :: * -> *) (m :: * -> *) a b. (Foldable t, Monad m) => (a -> m b) -> t a -> m () mapM_ Con -> CompTrans () checkUniqueVar [Con] cons Maybe AnnotationPropInfo Nothing -> () -> CompTrans () forall a. a -> CompTrans a forall (m :: * -> *) a. Monad m => a -> m a return () [Con] cons' <- (Con -> CompTrans Con) -> [Con] -> CompTrans [Con] forall (t :: * -> *) (m :: * -> *) a b. (Traversable t, Monad m) => (a -> m b) -> t a -> m (t b) forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b] mapM (Name -> Name -> Name -> Con -> CompTrans Con mkCon Name n' Name e Name i) [Con] cons return $ [Cxt -> Name -> [TyVarBndr BndrVis] -> Maybe Type -> [Con] -> [DerivClause] -> Dec DataD [] Name n' [Name -> BndrVis -> Type -> TyVarBndr BndrVis forall flag. Name -> flag -> Type -> TyVarBndr flag KindedTV Name e BndrVis BndrReq (Type -> Type -> Type AppT (Type -> Type -> Type AppT Type ArrowT Type StarT) Type StarT), Name -> BndrVis -> TyVarBndr BndrVis forall flag. Name -> flag -> TyVarBndr flag PlainTV Name i BndrVis BndrReq] Maybe Type forall a. Maybe a Nothing [Con] cons' [] ,Cxt -> Name -> [TyVarBndr BndrVis] -> Maybe Type -> [Con] -> [DerivClause] -> Dec DataD [] (Name -> Name nameLab Name n) [] Maybe Type forall a. Maybe a Nothing [] [] ] mkCon :: Name -> Name -> Name -> Con -> CompTrans Con mkCon :: Name -> Name -> Name -> Con -> CompTrans Con mkCon Name l Name e Name i (NormalC Name n [BangType] sts) = Getting (Maybe AnnotationPropInfo) TransCtx (Maybe AnnotationPropInfo) -> CompTrans (Maybe AnnotationPropInfo) forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a view Getting (Maybe AnnotationPropInfo) TransCtx (Maybe AnnotationPropInfo) forall c. HasTransCtx c => Lens' c (Maybe AnnotationPropInfo) Lens' TransCtx (Maybe AnnotationPropInfo) annotationProp CompTrans (Maybe AnnotationPropInfo) -> (Maybe AnnotationPropInfo -> CompTrans Con) -> CompTrans Con forall a b. CompTrans a -> (a -> CompTrans b) -> CompTrans b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= Maybe AnnotationPropInfo -> CompTrans Con mkConNormal where mkConNormal :: Maybe AnnotationPropInfo -> CompTrans Con mkConNormal Maybe AnnotationPropInfo annPropInfo = [TyVarBndr Specificity] -> Cxt -> Con -> Con ForallC [] Cxt ctx (Con -> Con) -> CompTrans Con -> CompTrans Con forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> CompTrans Con inner where ctx :: Cxt ctx = [(Type -> Type -> Type) -> Type -> Cxt -> Type forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl Type -> Type -> Type AppT Type EqualityT [(Name -> Type VarT Name i), (Name -> Type ConT (Name -> Type) -> Name -> Type forall a b. (a -> b) -> a -> b $ Name -> Name nameLab Name l)]] sts' :: [BangType] sts' = case Maybe AnnotationPropInfo annPropInfo of Just AnnotationPropInfo api -> (BangType -> Bool) -> [BangType] -> [BangType] forall a. (a -> Bool) -> [a] -> [a] filter (Bool -> Bool not (Bool -> Bool) -> (BangType -> Bool) -> BangType -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . (AnnotationPropInfo api AnnotationPropInfo -> Getting (Type -> Bool) AnnotationPropInfo (Type -> Bool) -> Type -> Bool forall s a. s -> Getting a s a -> a ^. Getting (Type -> Bool) AnnotationPropInfo (Type -> Bool) forall c. HasAnnotationPropInfo c => Lens' c (Type -> Bool) Lens' AnnotationPropInfo (Type -> Bool) isAnnotation) (Type -> Bool) -> (BangType -> Type) -> BangType -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . (BangType -> Getting Type BangType Type -> Type forall s a. s -> Getting a s a -> a ^. Getting Type BangType Type forall s t a b. Field2 s t a b => Lens s t a b Lens BangType BangType Type Type _2)) [BangType] sts Maybe AnnotationPropInfo Nothing -> [BangType] sts sts'' :: CompTrans [BangType] sts'' = [BangType] sts' [BangType] -> ([BangType] -> CompTrans [BangType]) -> CompTrans [BangType] forall a b. a -> (a -> b) -> b & ((BangType -> CompTrans BangType) -> [BangType] -> CompTrans [BangType] forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> [a] -> f [b] traverse((BangType -> CompTrans BangType) -> [BangType] -> CompTrans [BangType]) -> ((Type -> CompTrans Type) -> BangType -> CompTrans BangType) -> (Type -> CompTrans Type) -> [BangType] -> CompTrans [BangType] forall b c a. (b -> c) -> (a -> b) -> a -> c .(Type -> CompTrans Type) -> BangType -> CompTrans BangType forall s t a b. Field2 s t a b => Lens s t a b Lens BangType BangType Type Type _2) ((Type -> CompTrans Type) -> [BangType] -> CompTrans [BangType]) -> (Type -> CompTrans Type) -> [BangType] -> CompTrans [BangType] forall {k} (f :: k -> *) s (t :: k) a (b :: k). LensLike f s t a b -> LensLike f s t a b %%~ Name -> Type -> CompTrans Type unfixType Name e inner :: CompTrans Con inner = ([BangType] -> Con) -> CompTrans [BangType] -> CompTrans Con forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r liftM (Name -> [BangType] -> Con NormalC (Name -> Name transName Name n)) CompTrans [BangType] sts'' mkCon Name l Name e Name i (RecC Name n [VarBangType] vsts) = Getting (Maybe AnnotationPropInfo) TransCtx (Maybe AnnotationPropInfo) -> CompTrans (Maybe AnnotationPropInfo) forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a view Getting (Maybe AnnotationPropInfo) TransCtx (Maybe AnnotationPropInfo) forall c. HasTransCtx c => Lens' c (Maybe AnnotationPropInfo) Lens' TransCtx (Maybe AnnotationPropInfo) annotationProp CompTrans (Maybe AnnotationPropInfo) -> (Maybe AnnotationPropInfo -> CompTrans Con) -> CompTrans Con forall a b. CompTrans a -> (a -> CompTrans b) -> CompTrans b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= Maybe AnnotationPropInfo -> CompTrans Con mkConRec where mkConRec :: Maybe AnnotationPropInfo -> CompTrans Con mkConRec Maybe AnnotationPropInfo annPropInfo = [TyVarBndr Specificity] -> Cxt -> Con -> Con ForallC [] Cxt ctx (Con -> Con) -> CompTrans Con -> CompTrans Con forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> CompTrans Con inner where ctx :: Cxt ctx = [(Type -> Type -> Type) -> Type -> Cxt -> Type forall b a. (b -> a -> b) -> b -> [a] -> b forall (t :: * -> *) b a. Foldable t => (b -> a -> b) -> b -> t a -> b foldl Type -> Type -> Type AppT Type EqualityT [(Name -> Type VarT Name i), (Name -> Type ConT (Name -> Type) -> Name -> Type forall a b. (a -> b) -> a -> b $ Name -> Name nameLab Name l)]] vsts' :: [VarBangType] vsts' = case Maybe AnnotationPropInfo annPropInfo of Just AnnotationPropInfo api -> (VarBangType -> Bool) -> [VarBangType] -> [VarBangType] forall a. (a -> Bool) -> [a] -> [a] filter (Bool -> Bool not (Bool -> Bool) -> (VarBangType -> Bool) -> VarBangType -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . (AnnotationPropInfo api AnnotationPropInfo -> Getting (Type -> Bool) AnnotationPropInfo (Type -> Bool) -> Type -> Bool forall s a. s -> Getting a s a -> a ^. Getting (Type -> Bool) AnnotationPropInfo (Type -> Bool) forall c. HasAnnotationPropInfo c => Lens' c (Type -> Bool) Lens' AnnotationPropInfo (Type -> Bool) isAnnotation) (Type -> Bool) -> (VarBangType -> Type) -> VarBangType -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . (VarBangType -> Getting Type VarBangType Type -> Type forall s a. s -> Getting a s a -> a ^. Getting Type VarBangType Type forall s t a b. Field3 s t a b => Lens s t a b Lens VarBangType VarBangType Type Type _3)) [VarBangType] vsts Maybe AnnotationPropInfo Nothing -> [VarBangType] vsts vsts'' :: [VarBangType] vsts'' = [VarBangType] vsts' [VarBangType] -> ([VarBangType] -> [VarBangType]) -> [VarBangType] forall a b. a -> (a -> b) -> b & ((VarBangType -> Identity VarBangType) -> [VarBangType] -> Identity [VarBangType] forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> [a] -> f [b] traverse((VarBangType -> Identity VarBangType) -> [VarBangType] -> Identity [VarBangType]) -> ((Name -> Identity Name) -> VarBangType -> Identity VarBangType) -> (Name -> Identity Name) -> [VarBangType] -> Identity [VarBangType] forall b c a. (b -> c) -> (a -> b) -> a -> c .(Name -> Identity Name) -> VarBangType -> Identity VarBangType forall s t a b. Field1 s t a b => Lens s t a b Lens VarBangType VarBangType Name Name _1) ((Name -> Identity Name) -> [VarBangType] -> Identity [VarBangType]) -> (Name -> Name) -> [VarBangType] -> [VarBangType] forall s t a b. ASetter s t a b -> (a -> b) -> s -> t %~ Name -> Name transName vsts''' :: CompTrans [VarBangType] vsts''' = [VarBangType] vsts'' [VarBangType] -> ([VarBangType] -> CompTrans [VarBangType]) -> CompTrans [VarBangType] forall a b. a -> (a -> b) -> b & ((VarBangType -> CompTrans VarBangType) -> [VarBangType] -> CompTrans [VarBangType] forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) forall (f :: * -> *) a b. Applicative f => (a -> f b) -> [a] -> f [b] traverse((VarBangType -> CompTrans VarBangType) -> [VarBangType] -> CompTrans [VarBangType]) -> ((Type -> CompTrans Type) -> VarBangType -> CompTrans VarBangType) -> (Type -> CompTrans Type) -> [VarBangType] -> CompTrans [VarBangType] forall b c a. (b -> c) -> (a -> b) -> a -> c .(Type -> CompTrans Type) -> VarBangType -> CompTrans VarBangType forall s t a b. Field3 s t a b => Lens s t a b Lens VarBangType VarBangType Type Type _3) ((Type -> CompTrans Type) -> [VarBangType] -> CompTrans [VarBangType]) -> (Type -> CompTrans Type) -> [VarBangType] -> CompTrans [VarBangType] forall {k} (f :: k -> *) s (t :: k) a (b :: k). LensLike f s t a b -> LensLike f s t a b %%~ Name -> Type -> CompTrans Type unfixType Name e inner :: CompTrans Con inner = ([VarBangType] -> Con) -> CompTrans [VarBangType] -> CompTrans Con forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r liftM (Name -> [VarBangType] -> Con RecC (Name -> Name transName Name n)) CompTrans [VarBangType] vsts''' mkCon Name _ Name _ Name _ Con c = [Char] -> CompTrans Con forall a. [Char] -> CompTrans a forall (m :: * -> *) a. MonadFail m => [Char] -> m a fail ([Char] -> CompTrans Con) -> [Char] -> CompTrans Con forall a b. (a -> b) -> a -> b $ [Char] "Attempted to derive multi-sorted compositional datatype for something with non-normal constructors: " [Char] -> [Char] -> [Char] forall a. [a] -> [a] -> [a] ++ Con -> [Char] forall a. Show a => a -> [Char] show Con c unfixType :: Name -> Type -> CompTrans Type unfixType :: Name -> Type -> CompTrans Type unfixType Name _ Type t | Type -> Cxt -> Bool forall a. Eq a => a -> [a] -> Bool forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool elem Type t Cxt baseTypes = Type -> CompTrans Type forall a. a -> CompTrans a forall (m :: * -> *) a. Monad m => a -> m a return Type t unfixType Name e Type t = do Type -> Bool checkAnn <- CompTrans (Type -> Bool) getIsAnn Type t' <- (ReaderT TransCtx Q Type -> CompTrans Type forall a. ReaderT TransCtx Q a -> CompTrans a CompTrans (ReaderT TransCtx Q Type -> CompTrans Type) -> ReaderT TransCtx Q Type -> CompTrans Type forall a b. (a -> b) -> a -> b $ Q Type -> ReaderT TransCtx Q Type forall (m :: * -> *) a. Monad m => m a -> ReaderT TransCtx m a forall (t :: (* -> *) -> * -> *) (m :: * -> *) a. (MonadTrans t, Monad m) => m a -> t m a lift (Type -> Q Type expandSyns Type t)) CompTrans Type -> (Type -> CompTrans Type) -> CompTrans Type forall a b. CompTrans a -> (a -> CompTrans b) -> CompTrans b forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b >>= (Type -> Bool) -> Type -> CompTrans Type getLab Type -> Bool checkAnn return $ Type -> Type -> Type AppT (Name -> Type VarT Name e) Type t'