diff --git a/cabal.project b/cabal.project index f0d40704..618c6f88 100644 --- a/cabal.project +++ b/cabal.project @@ -4,4 +4,4 @@ packages: . source-repository-package type: git location: https://github.com/goldfirere/th-desugar - tag: 567145eddeb5f6692a75e74d4a2dc575b1ad6f29 + tag: 8495349a53f4bc3bde30378f2d85a07aae53bdbd diff --git a/src/Data/Singletons/CustomStar.hs b/src/Data/Singletons/CustomStar.hs index 7e41262f..5a38bd97 100644 --- a/src/Data/Singletons/CustomStar.hs +++ b/src/Data/Singletons/CustomStar.hs @@ -76,7 +76,7 @@ singletonStar names = do kinds <- mapM getKind names ctors <- zipWithM (mkCtor True) names kinds let repDecl = DDataD Data [] repName [] (Just (DConT typeKindName)) ctors - [DDerivClause Nothing (map DConPr [''Eq, ''Ord, ''Read, ''Show])] + [DDerivClause Nothing (map DConT [''Eq, ''Ord, ''Read, ''Show])] fakeCtors <- zipWithM (mkCtor False) names kinds let dataDecl = DataDecl repName [] fakeCtors -- Why do we need withLocalDeclarations here? It's because we end up @@ -86,7 +86,7 @@ singletonStar names = do withLocalDeclarations (decToTH repDecl) $ do -- We opt to infer the constraints for the Eq instance here so that when it's -- promoted, Rep will be promoted to Type. - dataDeclEqCxt <- inferConstraints (DConPr ''Eq) (DConT repName) fakeCtors + dataDeclEqCxt <- inferConstraints (DConT ''Eq) (DConT repName) fakeCtors let dataDeclEqInst = DerivedDecl (Just dataDeclEqCxt) (DConT repName) dataDecl ordInst <- mkOrdInstance Nothing (DConT repName) dataDecl showInst <- mkShowInstance Nothing (DConT repName) dataDecl diff --git a/src/Data/Singletons/Deriving/Bounded.hs b/src/Data/Singletons/Deriving/Bounded.hs index 4738fe2e..b9f8c596 100644 --- a/src/Data/Singletons/Deriving/Bounded.hs +++ b/src/Data/Singletons/Deriving/Bounded.hs @@ -50,7 +50,7 @@ mkBoundedInstance mb_ctxt ty (DataDecl _ _ cons) = do in (minEqnRHS, maxEqnRHS) mk_rhs rhs = UFunction [DClause [] rhs] - constraints <- inferConstraintsDef mb_ctxt (DConPr boundedName) ty cons + constraints <- inferConstraintsDef mb_ctxt (DConT boundedName) ty cons return $ InstDecl { id_cxt = constraints , id_name = boundedName , id_arg_tys = [ty] diff --git a/src/Data/Singletons/Deriving/Enum.hs b/src/Data/Singletons/Deriving/Enum.hs index b91a3eef..eebcf769 100644 --- a/src/Data/Singletons/Deriving/Enum.hs +++ b/src/Data/Singletons/Deriving/Enum.hs @@ -33,15 +33,15 @@ mkEnumInstance mb_ctxt ty (DataDecl data_name tvbs cons) = do non_vanilla || not (null $ tysOfConFields f)) cons) $ fail ("Can't derive Enum instance for " ++ pprint (typeToTH ty) ++ ".") n <- qNewName "n" - let to_enum = UFunction [DClause [DVarPa n] (to_enum_rhs cons [0..])] + let to_enum = UFunction [DClause [DVarP n] (to_enum_rhs cons [0..])] to_enum_rhs [] _ = DVarE errorName `DAppE` DLitE (StringL "toEnum: bad argument") to_enum_rhs (DCon _ _ name _ _ : rest) (num:nums) = DCaseE (DVarE equalsName `DAppE` DVarE n `DAppE` DLitE (IntegerL num)) - [ DMatch (DConPa trueName []) (DConE name) - , DMatch (DConPa falseName []) (to_enum_rhs rest nums) ] + [ DMatch (DConP trueName []) (DConE name) + , DMatch (DConP falseName []) (to_enum_rhs rest nums) ] to_enum_rhs _ _ = error "Internal error: exhausted infinite list in to_enum_rhs" - from_enum = UFunction (zipWith (\i con -> DClause [DConPa (extractName con) []] + from_enum = UFunction (zipWith (\i con -> DClause [DConP (extractName con) []] (DLitE (IntegerL i))) [0..] cons) return (InstDecl { id_cxt = fromMaybe [] mb_ctxt diff --git a/src/Data/Singletons/Deriving/Foldable.hs b/src/Data/Singletons/Deriving/Foldable.hs index a88ce7b2..af262fd7 100644 --- a/src/Data/Singletons/Deriving/Foldable.hs +++ b/src/Data/Singletons/Deriving/Foldable.hs @@ -69,17 +69,17 @@ mkFoldableInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do mk_foldMap_clause :: DCon -> q DClause mk_foldMap_clause con = do parts <- foldDataConArgs ft_foldMap con - clause_for_foldMap [DVarPa f] con =<< sequence parts + clause_for_foldMap [DVarP f] con =<< sequence parts mk_foldr_clause :: DCon -> q DClause mk_foldr_clause con = do parts <- foldDataConArgs ft_foldr con - clause_for_foldr [DVarPa f, DVarPa z] con =<< sequence parts + clause_for_foldr [DVarP f, DVarP z] con =<< sequence parts mk_foldMap :: q [DClause] mk_foldMap = case cons of - [] -> pure [DClause [DWildPa, DWildPa] (DVarE memptyName)] + [] -> pure [DClause [DWildP, DWildP] (DVarE memptyName)] _ -> traverse mk_foldMap_clause cons mk_foldr :: q [DClause] @@ -91,7 +91,7 @@ mkFoldableInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do : case cons of [] -> [] _ -> [(foldrName, UFunction foldr_clauses)] - constraints <- inferConstraintsDef mb_ctxt (DConPr foldableName) ty cons + constraints <- inferConstraintsDef mb_ctxt (DConT foldableName) ty cons return $ InstDecl { id_cxt = constraints , id_name = foldableName , id_arg_tys = [ty] diff --git a/src/Data/Singletons/Deriving/Functor.hs b/src/Data/Singletons/Deriving/Functor.hs index 937f1c0c..705c4531 100644 --- a/src/Data/Singletons/Deriving/Functor.hs +++ b/src/Data/Singletons/Deriving/Functor.hs @@ -61,28 +61,28 @@ mkFunctorInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do mk_fmap_clause :: DCon -> q DClause mk_fmap_clause con = do parts <- foldDataConArgs ft_fmap con - clause_for_con [DVarPa f] con =<< sequence parts + clause_for_con [DVarP f] con =<< sequence parts mk_replace_clause :: DCon -> q DClause mk_replace_clause con = do parts <- foldDataConArgs ft_replace con - clause_for_con [DVarPa z] con =<< traverse (fmap replace) parts + clause_for_con [DVarP z] con =<< traverse (fmap replace) parts mk_fmap :: q [DClause] mk_fmap = case cons of [] -> do v <- newUniqueName "v" - pure [DClause [DWildPa, DVarPa v] (DCaseE (DVarE v) [])] + pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])] _ -> traverse mk_fmap_clause cons mk_replace :: q [DClause] mk_replace = case cons of [] -> do v <- newUniqueName "v" - pure [DClause [DWildPa, DVarPa v] (DCaseE (DVarE v) [])] + pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])] _ -> traverse mk_replace_clause cons fmap_clauses <- mk_fmap replace_clauses <- mk_replace - constraints <- inferConstraintsDef mb_ctxt (DConPr functorName) ty cons + constraints <- inferConstraintsDef mb_ctxt (DConT functorName) ty cons return $ InstDecl { id_cxt = constraints , id_name = functorName , id_arg_tys = [ty] diff --git a/src/Data/Singletons/Deriving/Infer.hs b/src/Data/Singletons/Deriving/Infer.hs index fe7527a9..a9ca588c 100644 --- a/src/Data/Singletons/Deriving/Infer.hs +++ b/src/Data/Singletons/Deriving/Infer.hs @@ -128,7 +128,7 @@ inferConstraints pr inst_ty = fmap (nubBy geq) . concatMapM infer_ct Just subst -> traverse (substTy subst) field_tys if is_functor_like then mk_functor_like_constraints field_tys' res_ty' - else pure $ map (pr `DAppPr`) field_tys' + else pure $ map (pr `DAppT`) field_tys' -- If we derive a Functor-like class, e.g., -- @@ -146,11 +146,11 @@ inferConstraints pr inst_ty = fmap (nubBy geq) . concatMapM infer_ct (_, last_res_ty_arg) = snocView res_ty_args Just last_tv = getDVarTName_maybe last_res_ty_arg deep_subtypes <- concatMapM (deepSubtypesContaining last_tv) fields - pure $ map (pr `DAppPr`) deep_subtypes + pure $ map (pr `DAppT`) deep_subtypes is_functor_like :: Bool is_functor_like - | DConT pr_class_name :| _ <- unfoldType (predToType pr) + | DConT pr_class_name :| _ <- unfoldType pr = isFunctorLikeClassName pr_class_name | otherwise = False diff --git a/src/Data/Singletons/Deriving/Ord.hs b/src/Data/Singletons/Deriving/Ord.hs index 302e9848..6bca295a 100644 --- a/src/Data/Singletons/Deriving/Ord.hs +++ b/src/Data/Singletons/Deriving/Ord.hs @@ -24,7 +24,7 @@ import Data.Singletons.Syntax -- | Make a *non-singleton* Ord instance mkOrdInstance :: DsMonad q => DerivDesc q mkOrdInstance mb_ctxt ty (DataDecl _ _ cons) = do - constraints <- inferConstraintsDef mb_ctxt (DConPr ordName) ty cons + constraints <- inferConstraintsDef mb_ctxt (DConT ordName) ty cons compare_eq_clauses <- mapM mk_equal_clause cons let compare_noneq_clauses = map (uncurry mk_nonequal_clause) [ (con1, con2) @@ -45,8 +45,8 @@ mk_equal_clause (DCon _tvbs _cxt name fields _rty) = do let tys = tysOfConFields fields a_names <- mapM (const $ newUniqueName "a") tys b_names <- mapM (const $ newUniqueName "b") tys - let pat1 = DConPa name (map DVarPa a_names) - pat2 = DConPa name (map DVarPa b_names) + let pat1 = DConP name (map DVarP a_names) + pat2 = DConP name (map DVarP b_names) return $ DClause [pat1, pat2] (DVarE foldlName `DAppE` DVarE thenCmpName `DAppE` DConE cmpEQName `DAppE` @@ -63,9 +63,9 @@ mk_nonequal_clause (DCon _tvbs1 _cxt1 name1 fields1 _rty1, n1) EQ -> DConE cmpEQName GT -> DConE cmpGTName) where - pat1 = DConPa name1 (map (const DWildPa) (tysOfConFields fields1)) - pat2 = DConPa name2 (map (const DWildPa) (tysOfConFields fields2)) + pat1 = DConP name1 (map (const DWildP) (tysOfConFields fields1)) + pat2 = DConP name2 (map (const DWildP) (tysOfConFields fields2)) -- A variant of mk_equal_clause tailored to empty datatypes mk_empty_clause :: DClause -mk_empty_clause = DClause [DWildPa, DWildPa] (DConE cmpEQName) +mk_empty_clause = DClause [DWildP, DWildP] (DConE cmpEQName) diff --git a/src/Data/Singletons/Deriving/Show.hs b/src/Data/Singletons/Deriving/Show.hs index c7984584..b7dc93bf 100644 --- a/src/Data/Singletons/Deriving/Show.hs +++ b/src/Data/Singletons/Deriving/Show.hs @@ -30,7 +30,7 @@ import GHC.Show (appPrec, appPrec1) mkShowInstance :: DsMonad q => DerivDesc q mkShowInstance mb_ctxt ty (DataDecl _ _ cons) = do clauses <- mk_showsPrec cons - constraints <- inferConstraintsDef mb_ctxt (DConPr showName) ty cons + constraints <- inferConstraintsDef mb_ctxt (DConT showName) ty cons return $ InstDecl { id_cxt = constraints , id_name = showName , id_arg_tys = [ty] @@ -42,7 +42,7 @@ mk_showsPrec cons = do p <- newUniqueName "p" -- The precedence argument (not always used) if null cons then do v <- newUniqueName "v" - pure [DClause [DWildPa, DVarPa v] (DCaseE (DVarE v) [])] + pure [DClause [DWildP, DVarP v] (DCaseE (DVarE v) [])] else mapM (mk_showsPrec_clause p) cons mk_showsPrec_clause :: forall q. DsMonad q @@ -54,7 +54,7 @@ mk_showsPrec_clause p (DCon _ _ con_name con_fields _) = go con_fields -- No fields: print just the constructor name, with no parentheses go (DNormalC _ []) = return $ - DClause [DWildPa, DConPa con_name []] $ + DClause [DWildP, DConP con_name []] $ DVarE showStringName `DAppE` dStringE (parenInfixConName con_name "") -- Infix constructors have special Show treatment. @@ -70,7 +70,7 @@ mk_showsPrec_clause p (DCon _ _ con_name con_fields _) = go con_fields -- Make sure to handle infix data constructors -- like (Int `Foo` Int) else " `" ++ op_name ++ "` " - return $ DClause [DVarPa p, DConPa con_name [DVarPa argL, DVarPa argR]] $ + return $ DClause [DVarP p, DConP con_name [DVarP argL, DVarP argR]] $ (DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE con_prec)) `DAppE` (DVarE composeName @@ -91,7 +91,7 @@ mk_showsPrec_clause p (DCon _ _ con_name con_fields _) = go con_fields `DAppE` (DVarE showStringName `DAppE` dStringE (parenInfixConName con_name " ")) `DAppE` composed_args - return $ DClause [DVarPa p, DConPa con_name $ map DVarPa args] $ + return $ DClause [DVarP p, DConP con_name $ map DVarP args] $ DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) `DAppE` named_args @@ -121,7 +121,7 @@ mk_showsPrec_clause p (DCon _ _ con_name con_fields _) = go con_fields `DAppE` (DVarE showStringName `DAppE` dStringE (parenInfixConName con_name " ")) `DAppE` composed_args - return $ DClause [DVarPa p, DConPa con_name $ map DVarPa args] $ + return $ DClause [DVarP p, DConP con_name $ map DVarP args] $ DVarE showParenName `DAppE` (DVarE gtName `DAppE` DVarE p `DAppE` dIntegerE appPrec) `DAppE` named_args @@ -156,7 +156,7 @@ mkShowSingContext :: DCxt -> DCxt mkShowSingContext = map show_to_SingShow where show_to_SingShow :: DPred -> DPred - show_to_SingShow = modifyConNameDPred $ \n -> + show_to_SingShow = modifyConNameDType $ \n -> if n == showName then showSingName else n diff --git a/src/Data/Singletons/Deriving/Traversable.hs b/src/Data/Singletons/Deriving/Traversable.hs index 1dd5ebee..cad30ff7 100644 --- a/src/Data/Singletons/Deriving/Traversable.hs +++ b/src/Data/Singletons/Deriving/Traversable.hs @@ -51,17 +51,17 @@ mkTraversableInstance mb_ctxt ty dd@(DataDecl _ _ cons) = do mk_trav_clause :: DCon -> q DClause mk_trav_clause con = do parts <- foldDataConArgs ft_trav con - clause_for_con [DVarPa f] con =<< sequence parts + clause_for_con [DVarP f] con =<< sequence parts mk_trav :: q [DClause] mk_trav = case cons of [] -> do v <- newUniqueName "v" - pure [DClause [DWildPa, DVarPa v] + pure [DClause [DWildP, DVarP v] (DVarE pureName `DAppE` DCaseE (DVarE v) [])] _ -> traverse mk_trav_clause cons trav_clauses <- mk_trav - constraints <- inferConstraintsDef mb_ctxt (DConPr traversableName) ty cons + constraints <- inferConstraintsDef mb_ctxt (DConT traversableName) ty cons return $ InstDecl { id_cxt = constraints , id_name = traversableName , id_arg_tys = [ty] diff --git a/src/Data/Singletons/Deriving/Util.hs b/src/Data/Singletons/Deriving/Util.hs index 051c5b2e..84de8c9e 100644 --- a/src/Data/Singletons/Deriving/Util.hs +++ b/src/Data/Singletons/Deriving/Util.hs @@ -208,7 +208,7 @@ functorLikeValidityChecks allowConstrainedLastTyVar (DataDecl n data_tvbs cons) = do ex_tvbs <- conExistentialTvbs (foldTypeTvbs (DConT n) data_tvbs) con let univ_tvb_names = map extractTvbName con_tvbs \\ map extractTvbName ex_tvbs if last_tv `elem` univ_tvb_names - && last_tv `Set.notMember` foldMap fvDPred con_theta + && last_tv `Set.notMember` foldMap fvDType con_theta then pure () else fail $ badCon con_name existential | otherwise @@ -297,7 +297,7 @@ mkSimpleConClause :: Quasi q -> q DClause mkSimpleConClause fold extra_pats (DCon _ _ con_name _ _) insides = do vars_needed <- replicateM (length insides) $ newUniqueName "a" - let pat = DConPa con_name (map DVarPa vars_needed) + let pat = DConP con_name (map DVarP vars_needed) rhs = fold con_name (zipWith (\i v -> i `DAppE` DVarE v) insides vars_needed) pure $ DClause (extra_pats ++ [pat]) rhs diff --git a/src/Data/Singletons/Names.hs b/src/Data/Singletons/Names.hs index 8b82b977..7c8451a2 100644 --- a/src/Data/Singletons/Names.hs +++ b/src/Data/Singletons/Names.hs @@ -285,7 +285,7 @@ singFamily :: DType singFamily = DConT singFamilyName singKindConstraint :: DKind -> DPred -singKindConstraint = DAppPr (DConPr singKindClassName) +singKindConstraint = DAppT (DConT singKindClassName) demote :: DType demote = DConT demoteName @@ -302,9 +302,9 @@ mkListE = foldApply :: DType -> [DType] -> DType foldApply = foldl apply --- make and equality predicate +-- make an equality predicate mkEqPred :: DType -> DType -> DPred -mkEqPred ty1 ty2 = foldPred (DConPr equalityName) [ty1, ty2] +mkEqPred ty1 ty2 = foldType (DConT equalityName) [ty1, ty2] -- | If a 'String' begins with one or more underscores, return -- @'Just' (us, rest)@, where @us@ contain all of the underscores at the @@ -315,16 +315,18 @@ splitUnderscores s = case span (== '_') s of ([], _) -> Nothing res -> Just res --- Walk a DPred, applying a function to all occurrences of constructor names. -modifyConNameDPred :: (Name -> Name) -> DPred -> DPred -modifyConNameDPred mod_con_name = go +-- Walk a DType, applying a function to all occurrences of constructor names. +modifyConNameDType :: (Name -> Name) -> DType -> DType +modifyConNameDType mod_con_name = go where - go (DForallPr tvbs cxt p) = DForallPr tvbs (map go cxt) (go p) - go (DAppPr p t) = DAppPr (go p) t - go (DSigPr p k) = DSigPr (go p) k - go p@(DVarPr _) = p - go (DConPr n) = DConPr (mod_con_name n) - go p@DWildCardPr = p + go (DForallT tvbs cxt p) = DForallT tvbs (map go cxt) (go p) + go (DAppT p t) = DAppT (go p) t + go (DSigT p k) = DSigT (go p) k + go p@(DVarT _) = p + go (DConT n) = DConT (mod_con_name n) + go p@DWildCardT = p + go p@(DLitT {}) = p + go p@DArrowT = p {- Note [Defunctionalization symbol suffixes] diff --git a/src/Data/Singletons/Partition.hs b/src/Data/Singletons/Partition.hs index 95503b1d..37b25ee0 100644 --- a/src/Data/Singletons/Partition.hs +++ b/src/Data/Singletons/Partition.hs @@ -89,9 +89,9 @@ partitionDec (DDataD _nd _cxt name tvbs mk cons derivings) = do $ concatMap flatten_clause derivings return $ mconcat $ derived_dec : derived_decs where - flatten_clause :: DDerivClause -> [(Maybe DDerivStrategy, DType)] + flatten_clause :: DDerivClause -> [(Maybe DDerivStrategy, DPred)] flatten_clause (DDerivClause strat preds) = - map (\p -> (strat, predToType p)) preds + map (\p -> (strat, p)) preds partitionDec (DClassD cxt name tvbs fds decs) = do (lde, otfs) <- concatMapM partitionClassDec decs @@ -155,7 +155,7 @@ partitionDec dec = partitionClassDec :: Monad m => DDec -> m (ULetDecEnv, [OpenTypeFamilyDecl]) partitionClassDec (DLetDec (DSigD name ty)) = pure (typeBinding name ty, mempty) -partitionClassDec (DLetDec (DValD (DVarPa name) exp)) = +partitionClassDec (DLetDec (DValD (DVarP name) exp)) = pure (valueBinding name (UValue exp), mempty) partitionClassDec (DLetDec (DFunD name clauses)) = pure (valueBinding name (UFunction clauses), mempty) @@ -177,7 +177,7 @@ partitionInstanceDec :: Monad m => DDec -> m ( Maybe (Name, ULetDecRHS) -- right-hand sides of methods , Map Name DType -- method type signatures ) -partitionInstanceDec (DLetDec (DValD (DVarPa name) exp)) = +partitionInstanceDec (DLetDec (DValD (DVarP name) exp)) = pure (Just (name, UValue exp), mempty) partitionInstanceDec (DLetDec (DFunD name clauses)) = pure (Just (name, UFunction clauses), mempty) @@ -196,7 +196,7 @@ partitionDeriving :: forall m. DsMonad m => Maybe DDerivStrategy -- ^ The deriving strategy, if present. - -> DType -- ^ The class being derived (e.g., 'Eq'), possibly applied to + -> DPred -- ^ The class being derived (e.g., 'Eq'), possibly applied to -- some number of arguments (e.g., @C Int Bool@). -> Maybe DCxt -- ^ @'Just' ctx@ if @ctx@ was provided via @StandaloneDeriving@. -- 'Nothing' if using a @deriving@ clause. diff --git a/src/Data/Singletons/Promote.hs b/src/Data/Singletons/Promote.hs index 5bd3b3e5..c8d800c8 100644 --- a/src/Data/Singletons/Promote.hs +++ b/src/Data/Singletons/Promote.hs @@ -351,13 +351,15 @@ promoteClassDec decl@(ClassDecl { cd_cxt = cxt promote_superclass_pred :: DPred -> PrM DPred promote_superclass_pred = go where - go (DForallPr {}) = fail "Cannot promote quantified constraints" - go (DAppPr pr ty) = DAppPr <$> go pr <*> promoteType ty - go (DSigPr pr _k) = go pr -- just ignore the kind; it can't matter - go (DVarPr name) = fail $ "Cannot promote ConstraintKinds variables like " - ++ show name - go (DConPr name) = return $ DConPr (promoteClassName name) - go DWildCardPr = return DWildCardPr + go (DForallT {}) = fail "Cannot promote quantified constraints" + go (DAppT pr ty) = DAppT <$> go pr <*> promoteType ty + go (DSigT pr _k) = go pr -- just ignore the kind; it can't matter + go (DVarT name) = fail $ "Cannot promote ConstraintKinds variables like " + ++ show name + go (DConT name) = return $ DConT (promoteClassName name) + go DWildCardT = return DWildCardT + go (DLitT {}) = fail "Type-level literal spotted at head of a constraint" + go DArrowT = fail "(->) spotted at head of a constraint" -- returns (unpromoted method name, ALetDecRHS) pairs promoteInstanceDec :: Map Name DType -> UInstDecl -> PrM AInstDecl @@ -633,8 +635,8 @@ promoteLetDecRHS m_rhs_ki type_env fix_env prefixes name (UValue exp) = do num_arrows ann_exp ) _ -> do names <- replicateM num_arrows (newUniqueName "a") - let pats = map DVarPa names - newArgs = map DVarE names + let pats = map DVarP names + newArgs = map DVarE names promoteLetDecRHS m_rhs_ki type_env fix_env prefixes name (UFunction [DClause pats (foldExp exp newArgs)]) @@ -675,8 +677,8 @@ promoteLetDecRHS m_rhs_ki type_env fix_env prefixes name (UFunction clauses) = d etaContractOrExpand ty_num_args clause_num_args (DClause pats exp) | n >= 0 = do -- Eta-expand names <- replicateM n (newUniqueName "a") - let newPats = map DVarPa names - newArgs = map DVarE names + let newPats = map DVarP names + newArgs = map DVarE names return $ DClause (pats ++ newPats) (foldExp exp newArgs) | otherwise = do -- Eta-contract let (clausePats, lamPats) = splitAt ty_num_args pats @@ -718,27 +720,27 @@ promoteMatch (DMatch pat exp) = do -- promotes a term pattern into a type pattern, accumulating bound variable names promotePat :: DPat -> QWithAux PromDPatInfos PrM (DType, ADPat) -promotePat (DLitPa lit) = (, ADLitPa lit) <$> promoteLitPat lit -promotePat (DVarPa name) = do +promotePat (DLitP lit) = (, ADLitP lit) <$> promoteLitPat lit +promotePat (DVarP name) = do -- term vars can be symbols... type vars can't! tyName <- mkTyName name tell $ PromDPatInfos [(name, tyName)] Set.empty - return (DVarT tyName, ADVarPa name) -promotePat (DConPa name pats) = do + return (DVarT tyName, ADVarP name) +promotePat (DConP name pats) = do (types, pats') <- mapAndUnzipM promotePat pats let name' = unboxed_tuple_to_tuple name - return (foldType (DConT name') types, ADConPa name pats') + return (foldType (DConT name') types, ADConP name pats') where unboxed_tuple_to_tuple n | Just deg <- unboxedTupleNameDegree_maybe n = tupleDataName deg | otherwise = n -promotePat (DTildePa pat) = do +promotePat (DTildeP pat) = do qReportWarning "Lazy pattern converted into regular pattern in promotion" - second ADTildePa <$> promotePat pat -promotePat (DBangPa pat) = do + second ADTildeP <$> promotePat pat +promotePat (DBangP pat) = do qReportWarning "Strict pattern converted into regular pattern in promotion" - second ADBangPa <$> promotePat pat -promotePat (DSigPa pat ty) = do + second ADBangP <$> promotePat pat +promotePat (DSigP pat ty) = do -- We must maintain the invariant that any promoted pattern signature must -- not have any wildcards in the underlying pattern. -- See Note [Singling pattern signatures]. @@ -746,8 +748,8 @@ promotePat (DSigPa pat ty) = do (promoted, pat') <- promotePat wildless_pat ki <- promoteType ty tell $ PromDPatInfos [] (fvDType ki) - return (DSigT promoted ki, ADSigPa promoted pat' ki) -promotePat DWildPa = return (DWildCardT, ADWildPa) + return (DSigT promoted ki, ADSigP promoted pat' ki) +promotePat DWildP = return (DWildCardT, ADWildP) promoteExp :: DExp -> PrM (DType, ADExp) promoteExp (DVarE name) = fmap (, ADVarE name) $ lookupVarE name diff --git a/src/Data/Singletons/Promote/Defun.hs b/src/Data/Singletons/Promote/Defun.hs index cc7d3036..09402d39 100644 --- a/src/Data/Singletons/Promote/Defun.hs +++ b/src/Data/Singletons/Promote/Defun.hs @@ -176,7 +176,7 @@ defunctionalize name m_fixity m_arg_tvbs' m_res_kind' = do tyfun_param = mk_tvb tyfun_name m_tyfun arg_names = map extractTvbName arg_params params = arg_params ++ [tyfun_param] - con_eq_ct = DConPr sameKindName `DAppPr` lhs `DAppPr` rhs + con_eq_ct = DConT sameKindName `DAppT` lhs `DAppT` rhs where lhs = foldType (DConT data_name) (map DVarT arg_names) `apply` (DVarT extra_name) rhs = foldType (DConT next_name) (map DVarT (arg_names ++ [extra_name])) diff --git a/src/Data/Singletons/Single.hs b/src/Data/Singletons/Single.hs index 106352e9..f5d9681b 100644 --- a/src/Data/Singletons/Single.hs +++ b/src/Data/Singletons/Single.hs @@ -314,7 +314,7 @@ singClassD (ClassDecl { cd_cxt = cls_cxt , lde_infix = fixities , lde_proms = promoted_defaults , lde_bound_kvs = meth_bound_kvs } }) = - bindContext [foldPredTvbs (DConPr cls_name) cls_tvbs] $ do + bindContext [foldTypeTvbs (DConT cls_name) cls_tvbs] $ do (sing_sigs, _, tyvar_names, cxts, res_kis, singIDefunss) <- unzip6 <$> zipWithM (singTySig no_meth_defns meth_sigs meth_bound_kvs) meth_names (map promoteValRhs meth_names) @@ -345,7 +345,7 @@ singClassD (ClassDecl { cd_cxt = cls_cxt add_constraints meth_name sty (_, bound_kvs) res_ki = do -- Maybe monad prom_dflt <- Map.lookup meth_name promoted_defaults - let default_pred = foldPred (DConPr equalityName) + let default_pred = foldType (DConT equalityName) -- NB: Need the res_ki here to prevent ambiguous -- kinds in result-inferred default methods. -- See #175 @@ -420,7 +420,7 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys Just inst_sig -> do -- We have an InstanceSig, so just single that type. Take care to -- avoid binding the variables bound by the instance head as well. - let inst_bound = foldMap fvDPred cxt <> foldMap fvDType inst_kis + let inst_bound = foldMap fvDType (cxt ++ inst_kis) (s_ty, tyvar_names, ctxt, res_ki) <- sing_meth_ty inst_bound inst_sig pure (s_ty, tyvar_names, ctxt, Just res_ki) Nothing -> case mb_s_info of @@ -435,7 +435,7 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys pure ( substType subst s_ty , map extractTvbName sing_tvbs - , map (substPred subst) ctxt + , map (substType subst) ctxt , m_res_ki ) _ -> do mb_info <- dsReify name @@ -559,7 +559,7 @@ singLetDecRHS bound_names cxts res_kis name ld_rhs = bindContext (Map.findWithDefault [] name cxts) $ case ld_rhs of AValue prom num_arrows exp -> - DValD (DVarPa (singValName name)) <$> + DValD (DVarP (singValName name)) <$> (wrapUnSingFun num_arrows prom <$> singExp exp (Map.lookup name res_kis)) AFunction prom_fun num_arrows clauses -> let tyvar_names = case Map.lookup name bound_names of @@ -603,21 +603,21 @@ singPat :: Map Name Name -- from term-level names to type-level names singPat var_proms = go where go :: ADPat -> QWithAux SingDSigPaInfos SgM DPat - go (ADLitPa _lit) = + go (ADLitP _lit) = fail "Singling of literal patterns not yet supported" - go (ADVarPa name) = do + go (ADVarP name) = do tyname <- case Map.lookup name var_proms of Nothing -> fail "Internal error: unknown variable when singling pattern" Just tyname -> return tyname - pure $ DVarPa (singValName name) `DSigPa` (singFamily `DAppT` DVarT tyname) - go (ADConPa name pats) = DConPa (singDataConName name) <$> mapM go pats - go (ADTildePa pat) = do + pure $ DVarP (singValName name) `DSigP` (singFamily `DAppT` DVarT tyname) + go (ADConP name pats) = DConP (singDataConName name) <$> mapM go pats + go (ADTildeP pat) = do qReportWarning "Lazy pattern converted into regular pattern during singleton generation." go pat - go (ADBangPa pat) = DBangPa <$> go pat - go (ADSigPa prom_pat pat ty) = do + go (ADBangP pat) = DBangP <$> go pat + go (ADSigP prom_pat pat ty) = do pat' <- go pat -- Normally, calling dPatToDExp would be dangerous, since it fails if the -- supplied pattern contains any wildcard patterns. However, promotePat @@ -627,7 +627,7 @@ singPat var_proms = go -- See Note [Singling pattern signatures]. addElement (dPatToDExp pat', DSigT prom_pat ty) pure pat' - go ADWildPa = pure DWildPa + go ADWildP = pure DWildP -- | If given a non-empty list of 'SingDSigPaInfos', construct a case expression -- that brings singleton equality constraints into scope via pattern-matching. @@ -638,7 +638,7 @@ mkSigPaCaseE exps_with_sigs exp | otherwise = let (exps, sigs) = unzip exps_with_sigs scrutinee = mkTupleDExp exps - pats = map (DSigPa DWildPa . DAppT (DConT singFamilyName)) sigs + pats = map (DSigP DWildP . DAppT (DConT singFamilyName)) sigs in DCaseE scrutinee [DMatch (mkTupleDPat pats) exp] -- Note [Annotate case return type] @@ -765,7 +765,7 @@ singExp (ADLamE ty_names prom_lam names exp) _res_ki = do -- So: build a case let caseExp = DCaseE (mkTupleDExp (map DVarE sNames)) [DMatch (mkTupleDPat - (map ((DWildPa `DSigPa`) . + (map ((DWildP `DSigP`) . (singFamily `DAppT`) . DVarT) ty_names)) exp'] return $ wrapSingFun (length names) prom_lam $ DLamE sNames caseExp @@ -805,7 +805,7 @@ singDerivedEqDecs (DerivedDecl { ded_mb_cxt = mb_ctxt -- Walk a DPred, replacing all occurrences of SEq with SDecide. sEqToSDecide :: DPred -> DPred -sEqToSDecide = modifyConNameDPred $ \n -> +sEqToSDecide = modifyConNameDType $ \n -> -- Why don't we directly compare n to sEqClassName? Because n is almost certainly -- produced from a call to singClassName, which uses unqualified Names. Ugh. if nameBase n == nameBase sEqClassName @@ -825,7 +825,7 @@ singDerivedShowDecs (DerivedDecl { ded_mb_cxt = mb_cxt -- Be careful: we want to generate an instance context that uses ShowSing, -- not SShow. show_cxt <- inferConstraintsDef (fmap mkShowSingContext mb_cxt) - (DConPr showSingName) + (DConT showSingName) ty cons let show_inst = DStandaloneDerivD Nothing show_cxt (DConT showName `DAppT` (singFamily `DAppT` DSigT (DVarT z) ty)) diff --git a/src/Data/Singletons/Single/Data.hs b/src/Data/Singletons/Single/Data.hs index 6b889904..fcb528fe 100644 --- a/src/Data/Singletons/Single/Data.hs +++ b/src/Data/Singletons/Single/Data.hs @@ -83,7 +83,7 @@ singDataD (DataDecl name tvbs ctors) = do let (cname, numArgs) = extractNameArgs c cname' <- mkConName cname varNames <- replicateM numArgs (qNewName "b") - return $ DClause [DConPa (singDataConName cname) (map DVarPa varNames)] + return $ DClause [DConP (singDataConName cname) (map DVarP varNames)] (foldExp (DConE cname') (map (DAppE (DVarE fromSingName) . DVarE) varNames)) @@ -98,9 +98,9 @@ singDataD (DataDecl name tvbs ctors) = do let varPats = zipWith mkToSingVarPat varNames promoted recursiveCalls = zipWith mkRecursiveCall varNames promoted return $ - DClause [DConPa cname' varPats] + DClause [DConP cname' varPats] (multiCase recursiveCalls - (map (DConPa someSingDataName . listify . DVarPa) + (map (DConP someSingDataName . listify . DVarP) svarNames) (DAppE (DConE someSingDataName) (foldExp (DConE (singDataConName cname)) @@ -108,7 +108,7 @@ singDataD (DataDecl name tvbs ctors) = do mkToSingVarPat :: Name -> DKind -> DPat mkToSingVarPat varName ki = - DSigPa (DVarPa varName) (DAppT (DConT demoteName) ki) + DSigP (DVarP varName) (DAppT (DConT demoteName) ki) mkRecursiveCall :: Name -> DKind -> DExp mkRecursiveCall var_name ki = @@ -118,13 +118,13 @@ singDataD (DataDecl name tvbs ctors) = do mkEmptyFromSingClause :: SgM DClause mkEmptyFromSingClause = do x <- qNewName "x" - pure $ DClause [DVarPa x] + pure $ DClause [DVarP x] $ DCaseE (DVarE x) [] mkEmptyToSingClause :: SgM DClause mkEmptyToSingClause = do x <- qNewName "x" - pure $ DClause [DVarPa x] + pure $ DClause [DVarP x] $ DConE someSingDataName `DAppE` DCaseE (DVarE x) [] -- refine a constructor. @@ -153,10 +153,10 @@ singCtor (DCon _tvbs cxt name fields rty) -- SingI instance for data constructor emitDecs [DInstanceD Nothing - (map (DAppPr (DConPr singIName)) indices) + (map (DAppT (DConT singIName)) indices) (DAppT (DConT singIName) (foldType pCon kindedIndices)) - [DLetDec $ DValD (DVarPa singMethName) + [DLetDec $ DValD (DVarP singMethName) (foldExp sCon (map (const $ DVarE singMethName) types))]] -- SingI instances for defunctionalization symbols. Note that we don't -- support contexts in constructors at the moment, so it's fine for now to diff --git a/src/Data/Singletons/Single/Defun.hs b/src/Data/Singletons/Single/Defun.hs index 702ec247..bb2981d4 100644 --- a/src/Data/Singletons/Single/Defun.hs +++ b/src/Data/Singletons/Single/Defun.hs @@ -98,7 +98,7 @@ singDefuns n ns ty_ctxt mb_ty_args mb_ty_res = (map extractTvbName tvbs) singI_ctxt :: DCxt - singI_ctxt = map (DAppPr (DConPr singIName) . tvbToType) tvbs + singI_ctxt = map (DAppT (DConT singIName) . tvbToType) tvbs mk_inst_ty :: DType -> DType mk_inst_ty inst_head @@ -133,7 +133,7 @@ singDefuns n ns ty_ctxt mb_ty_args mb_ty_res = = DInstanceD Nothing (sty_ctxt ++ singI_ctxt) (DConT singIName `DAppT` mk_inst_ty inst_head) - [DLetDec $ DValD (DVarPa singMethName) + [DLetDec $ DValD (DVarP singMethName) $ wrapSingFun sing_fun_num inst_head $ mk_sing_fun_expr sing_exp ] diff --git a/src/Data/Singletons/Single/Eq.hs b/src/Data/Singletons/Single/Eq.hs index f50b5144..52cb1a91 100644 --- a/src/Data/Singletons/Single/Eq.hs +++ b/src/Data/Singletons/Single/Eq.hs @@ -31,7 +31,7 @@ mkEqualityInstance mb_ctxt k ctors sctors (mkMeth, mkEmpty, className, methName) methClauses <- if null sctors then (:[]) <$> mkEmpty else mapM mkMeth sctorPairs - constraints <- inferConstraintsDef mb_ctxt (DConPr className) k ctors + constraints <- inferConstraintsDef mb_ctxt (DConT className) k ctors return $ DInstanceD Nothing constraints (DAppT (DConT className) k) @@ -42,18 +42,18 @@ mkEqMethClause (c1, c2) | lname == rname = do lnames <- replicateM lNumArgs (qNewName "a") rnames <- replicateM lNumArgs (qNewName "b") - let lpats = map DVarPa lnames - rpats = map DVarPa rnames + let lpats = map DVarP lnames + rpats = map DVarP rnames lvars = map DVarE lnames rvars = map DVarE rnames return $ DClause - [DConPa lname lpats, DConPa rname rpats] + [DConP lname lpats, DConP rname rpats] (allExp (zipWith (\l r -> foldExp (DVarE sEqMethName) [l, r]) lvars rvars)) | otherwise = return $ DClause - [DConPa lname (replicate lNumArgs DWildPa), - DConPa rname (replicate rNumArgs DWildPa)] + [DConP lname (replicate lNumArgs DWildP), + DConP rname (replicate rNumArgs DWildP)] (DConE $ singDataConName falseName) where allExp :: [DExp] -> DExp allExp [] = DConE $ singDataConName trueName @@ -65,39 +65,39 @@ mkEqMethClause (c1, c2) mkEmptyEqMethClause :: Applicative q => q DClause mkEmptyEqMethClause = - pure $ DClause [DWildPa, DWildPa] + pure $ DClause [DWildP, DWildP] $ DConE strueName mkDecideMethClause :: Quasi q => (DCon, DCon) -> q DClause mkDecideMethClause (c1, c2) | lname == rname = if lNumArgs == 0 - then return $ DClause [DConPa lname [], DConPa rname []] + then return $ DClause [DConP lname [], DConP rname []] (DAppE (DConE provedName) (DConE reflName)) else do lnames <- replicateM lNumArgs (qNewName "a") rnames <- replicateM lNumArgs (qNewName "b") contra <- qNewName "contra" - let lpats = map DVarPa lnames - rpats = map DVarPa rnames + let lpats = map DVarP lnames + rpats = map DVarP rnames lvars = map DVarE lnames rvars = map DVarE rnames refl <- qNewName "refl" return $ DClause - [DConPa lname lpats, DConPa rname rpats] + [DConP lname lpats, DConP rname rpats] (DCaseE (mkTupleDExp $ zipWith (\l r -> foldExp (DVarE sDecideMethName) [l, r]) lvars rvars) ((DMatch (mkTupleDPat (replicate lNumArgs - (DConPa provedName [DConPa reflName []]))) + (DConP provedName [DConP reflName []]))) (DAppE (DConE provedName) (DConE reflName))) : - [DMatch (mkTupleDPat (replicate i DWildPa ++ - DConPa disprovedName [DVarPa contra] : - replicate (lNumArgs - i - 1) DWildPa)) + [DMatch (mkTupleDPat (replicate i DWildP ++ + DConP disprovedName [DVarP contra] : + replicate (lNumArgs - i - 1) DWildP)) (DAppE (DConE disprovedName) (DLamE [refl] $ DCaseE (DVarE refl) - [DMatch (DConPa reflName []) $ + [DMatch (DConP reflName []) $ (DAppE (DVarE contra) (DConE reflName))])) | i <- [0..lNumArgs-1] ])) @@ -105,8 +105,8 @@ mkDecideMethClause (c1, c2) | otherwise = do x <- qNewName "x" return $ DClause - [DConPa lname (replicate lNumArgs DWildPa), - DConPa rname (replicate rNumArgs DWildPa)] + [DConP lname (replicate lNumArgs DWildP), + DConP rname (replicate rNumArgs DWildP)] (DAppE (DConE disprovedName) (DLamE [x] (DCaseE (DVarE x) []))) where @@ -116,5 +116,5 @@ mkDecideMethClause (c1, c2) mkEmptyDecideMethClause :: Quasi q => q DClause mkEmptyDecideMethClause = do x <- qNewName "x" - pure $ DClause [DVarPa x, DWildPa] + pure $ DClause [DVarP x, DWildP] $ DConE provedName `DAppE` DCaseE (DVarE x) [] diff --git a/src/Data/Singletons/Single/Type.hs b/src/Data/Singletons/Single/Type.hs index 820987b1..ee9e5cc5 100644 --- a/src/Data/Singletons/Single/Type.hs +++ b/src/Data/Singletons/Single/Type.hs @@ -41,8 +41,8 @@ singType bound_kvs prom ty = do tau = ravel args' res' -- Make sure to subtract out the bound variables currently in scope, lest we -- accidentally shadow them in this type signature. - kv_names_to_bind = (foldMap fvDType prom_args <> foldMap fvDPred cxt' <> fvDType prom_res) - Set.\\ bound_kvs + kv_names_to_bind = foldMap fvDType (prom_args ++ cxt' ++ [prom_res]) + Set.\\ bound_kvs kvs_to_bind = Set.toList kv_names_to_bind let ty' = DForallT (map DPlainTV kvs_to_bind ++ zipWith DKindedTV arg_names prom_args) cxt' tau @@ -52,18 +52,22 @@ singPred :: DPred -> SgM DPred singPred = singPredRec [] singPredRec :: [DType] -> DPred -> SgM DPred -singPredRec _cxt (DForallPr {}) = +singPredRec _cxt (DForallT {}) = fail "Singling of quantified constraints not yet supported" -singPredRec ctx (DAppPr pr ty) = singPredRec (ty : ctx) pr -singPredRec _ctx (DSigPr _pr _ki) = +singPredRec ctx (DAppT pr ty) = singPredRec (ty : ctx) pr +singPredRec _ctx (DSigT _pr _ki) = fail "Singling of constraints with explicit kinds not yet supported" -singPredRec _ctx (DVarPr _n) = +singPredRec _ctx (DVarT _n) = fail "Singling of contraint variables not yet supported" -singPredRec ctx (DConPr n) +singPredRec ctx (DConT n) | n == equalityName = fail "Singling of type equality constraints not yet supported" | otherwise = do kis <- mapM promoteType ctx let sName = singClassName n - return $ foldPred (DConPr sName) kis -singPredRec _ctx DWildCardPr = return DWildCardPr -- it just might work + return $ foldType (DConT sName) kis +singPredRec _ctx DWildCardT = return DWildCardT -- it just might work +singPredRec _ctx DArrowT = + fail "(->) spotted at head of a constraint" +singPredRec _ctx (DLitT {}) = + fail "Type-level literal spotted at head of a constraint" diff --git a/src/Data/Singletons/Syntax.hs b/src/Data/Singletons/Syntax.hs index 33e4b023..6fcdbaa1 100644 --- a/src/Data/Singletons/Syntax.hs +++ b/src/Data/Singletons/Syntax.hs @@ -106,15 +106,15 @@ data ADExp = ADVarE Name ADExp DType -- A DPat with a pattern-signature node annotated with its type-level equivalent -data ADPat = ADLitPa Lit - | ADVarPa Name - | ADConPa Name [ADPat] - | ADTildePa ADPat - | ADBangPa ADPat - | ADSigPa DType -- The promoted pattern. Will not contain any wildcards, - -- as per Note [Singling pattern signatures] - ADPat DType - | ADWildPa +data ADPat = ADLitP Lit + | ADVarP Name + | ADConP Name [ADPat] + | ADTildeP ADPat + | ADBangP ADPat + | ADSigP DType -- The promoted pattern. Will not contain any wildcards, + -- as per Note [Singling pattern signatures] + ADPat DType + | ADWildP data ADMatch = ADMatch VarPromotions ADPat ADExp data ADClause = ADClause VarPromotions @@ -182,7 +182,7 @@ buildLetDecEnv = go emptyLetDecEnv go acc [] = return acc go acc (DFunD name clauses : rest) = go (valueBinding name (UFunction clauses) <> acc) rest - go acc (DValD (DVarPa name) exp : rest) = + go acc (DValD (DVarP name) exp : rest) = go (valueBinding name (UValue exp) <> acc) rest go acc (dec@(DValD {}) : rest) = do flattened <- flattenDValD dec diff --git a/src/Data/Singletons/TH.hs b/src/Data/Singletons/TH.hs index a8596d09..d141486e 100644 --- a/src/Data/Singletons/TH.hs +++ b/src/Data/Singletons/TH.hs @@ -189,4 +189,4 @@ buildCases ctor_infos expq bodyq = where conToPat :: (Name, Int) -> DPat conToPat (name, num_fields) = - DConPa name (replicate num_fields DWildPa) + DConP name (replicate num_fields DWildP) diff --git a/src/Data/Singletons/Util.hs b/src/Data/Singletons/Util.hs index 0f8f7887..fa8b715e 100644 --- a/src/Data/Singletons/Util.hs +++ b/src/Data/Singletons/Util.hs @@ -253,15 +253,6 @@ ravel :: [DType] -> DType -> DType ravel [] res = res ravel (h:t) res = DAppT (DAppT DArrowT h) (ravel t res) --- | Convert a 'DPred' to a 'DType'. -predToType :: DPred -> DType -predToType (DForallPr tvbs cxt p) = DForallT tvbs cxt (predToType p) -predToType (DAppPr p t) = DAppT (predToType p) t -predToType (DSigPr p k) = DSigT (predToType p) k -predToType (DVarPr n) = DVarT n -predToType (DConPr n) = DConT n -predToType DWildCardPr = DWildCardT - -- count the number of arguments in a type countArgs :: DType -> Int countArgs ty = length args @@ -298,7 +289,7 @@ substType subst (DForallT tvbs cxt inner_ty) = DForallT tvbs' cxt' inner_ty' where (subst', tvbs') = mapAccumL subst_tvb subst tvbs - cxt' = map (substPred subst') cxt + cxt' = map (substType subst') cxt inner_ty' = substType subst' inner_ty substType subst (DAppT ty1 ty2) = substType subst ty1 `DAppT` substType subst ty2 substType subst (DSigT ty ki) = substType subst ty `DSigT` substType subst ki @@ -311,22 +302,6 @@ substType _ ty@(DArrowT) = ty substType _ ty@(DLitT {}) = ty substType _ ty@DWildCardT = ty -substPred :: Map Name DType -> DPred -> DPred -substPred subst pred | Map.null subst = pred -substPred subst (DForallPr tvbs cxt inner_pred) - = DForallPr tvbs' cxt' inner_pred' - where - (subst', tvbs') = mapAccumL subst_tvb subst tvbs - cxt' = map (substPred subst') cxt - inner_pred' = substPred subst' inner_pred -substPred subst (DAppPr pred ty) = - DAppPr (substPred subst pred) (substType subst ty) -substPred subst (DSigPr pred ki) = - DSigPr (substPred subst pred) (substKind subst ki) -substPred _ pred@(DVarPr {}) = pred -substPred _ pred@(DConPr {}) = pred -substPred _ pred@DWildCardPr = pred - subst_tvb :: Map Name DKind -> DTyVarBndr -> (Map Name DKind, DTyVarBndr) subst_tvb s tvb@(DPlainTV n) = (Map.delete n s, tvb) subst_tvb s (DKindedTV n k) = (Map.delete n s, DKindedTV n (substKind s k)) @@ -343,14 +318,6 @@ foldType = foldl DAppT foldTypeTvbs :: DType -> [DTyVarBndr] -> DType foldTypeTvbs ty = foldType ty . map tvbToType --- apply a pred to a list of types -foldPred :: DPred -> [DType] -> DPred -foldPred = foldl DAppPr - --- apply a pred to a list of type variable binders -foldPredTvbs :: DPred -> [DTyVarBndr] -> DPred -foldPredTvbs pr = foldPred pr . map tvbToType - -- | Decompose an applied type into its individual components. For example, this: -- -- @