From 0cb7b227d9419e7896783a2773c285f7c980f816 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 25 Dec 2022 14:22:29 -0600 Subject: [PATCH] `singletons-th`: Remove unneeded kind annotation when singling `case` expressions Explicit kind annotations aren't necessary in modern `singletons-th` due to the approach that it uses for singling `case` expressions. This allows us to delete a modest amount of code. Fixes #547. --- .../GradingClient/Database.golden | 2 +- .../InsertionSort/InsertionSortImp.golden | 2 +- .../Singletons/CaseExpressions.golden | 10 +- .../Singletons/PatternMatching.golden | 10 +- .../compile-and-dump/Singletons/T150.golden | 2 +- .../compile-and-dump/Singletons/T160.golden | 2 +- .../compile-and-dump/Singletons/T183.golden | 2 +- .../Singletons/TopLevelPatterns.golden | 8 +- .../src/Data/Singletons/TH/Single.hs | 102 +++++++----------- .../src/Data/Singletons/TH/Single/Type.hs | 32 ++---- 10 files changed, 66 insertions(+), 106 deletions(-) diff --git a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden index 9a88c3c2..0ad9ef53 100644 --- a/singletons-base/tests/compile-and-dump/GradingClient/Database.golden +++ b/singletons-base/tests/compile-and-dump/GradingClient/Database.golden @@ -1444,7 +1444,7 @@ GradingClient/Database.hs:(0,0)-(0,0): Splicing declarations sName' in (GHC.Base.id - @(Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs) :: U))) + @(Sing (Case_0123456789876543210 name name' u attrs (Let0123456789876543210Scrutinee_0123456789876543210Sym4 name name' u attrs)))) (case sScrutinee_0123456789876543210 of STrue -> sU SFalse diff --git a/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden b/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden index 915cc4ea..c76368d1 100644 --- a/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden +++ b/singletons-base/tests/compile-and-dump/InsertionSort/InsertionSortImp.golden @@ -187,7 +187,7 @@ InsertionSort/InsertionSortImp.hs:(0,0)-(0,0): Splicing declarations = (applySing ((applySing ((singFun2 @LeqSym0) sLeq)) sN)) sH in (id - @(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t) :: [Nat]))) + @(Sing (Case_0123456789876543210 n h t (Let0123456789876543210Scrutinee_0123456789876543210Sym3 n h t)))) (case sScrutinee_0123456789876543210 of STrue -> (applySing ((applySing ((singFun2 @(:@#@$)) SCons)) sN)) diff --git a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden index 03ba7cc0..107066ff 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/CaseExpressions.golden @@ -245,7 +245,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations forall a (t :: a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply Foo1Sym0 t) t :: a) sFoo5 (sX :: Sing x) - = (id @(Sing (Case_0123456789876543210 x x :: a))) + = (id @(Sing (Case_0123456789876543210 x x))) (case sX of (sY :: Sing y) -> (applySing @@ -258,7 +258,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations (case sArg_0123456789876543210 of _ -> sX)))) sY) sFoo4 (sX :: Sing x) - = (id @(Sing (Case_0123456789876543210 x x :: a))) + = (id @(Sing (Case_0123456789876543210 x x))) (case sX of (sY :: Sing y) -> let @@ -273,7 +273,7 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations = (applySing ((applySing ((singFun2 @Tuple2Sym0) STuple2)) sA)) sB in (id - @(Sing (Case_0123456789876543210 a b (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a b) :: a))) + @(Sing (Case_0123456789876543210 a b (Let0123456789876543210Scrutinee_0123456789876543210Sym2 a b)))) (case sScrutinee_0123456789876543210 of STuple2 (sP :: Sing p) _ -> sP) sFoo2 (sD :: Sing d) _ @@ -284,10 +284,10 @@ Singletons/CaseExpressions.hs:(0,0)-(0,0): Splicing declarations = (applySing ((singFun1 @JustSym0) SJust)) sD in (id - @(Sing (Case_0123456789876543210 d (Let0123456789876543210Scrutinee_0123456789876543210Sym1 d) :: a))) + @(Sing (Case_0123456789876543210 d (Let0123456789876543210Scrutinee_0123456789876543210Sym1 d)))) (case sScrutinee_0123456789876543210 of SJust (sY :: Sing y) -> sY) sFoo1 (sD :: Sing d) (sX :: Sing x) - = (id @(Sing (Case_0123456789876543210 d x x :: a))) + = (id @(Sing (Case_0123456789876543210 d x x))) (case sX of SJust (sY :: Sing y) -> sY SNothing -> sD) diff --git a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden index e1e0f48d..b5dd1138 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/PatternMatching.golden @@ -471,7 +471,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations sSz :: Sing @_ SzSym0 sX_0123456789876543210 :: Sing @_ X_0123456789876543210Sym0 sSilly (sX :: Sing x) - = (id @(Sing (Case_0123456789876543210 x x :: ()))) + = (id @(Sing (Case_0123456789876543210 x x))) (case sX of _ -> STuple0) sFoo2 (STuple2 (sX :: Sing x) (sY :: Sing y)) = let @@ -480,7 +480,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations = (applySing ((applySing ((singFun2 @Tuple2Sym0) STuple2)) sX)) sY in (id - @(Sing (Case_0123456789876543210 x y (Let0123456789876543210TSym2 x y) :: a))) + @(Sing (Case_0123456789876543210 x y (Let0123456789876543210TSym2 x y)))) (case sT of STuple2 (sA :: Sing a) (sB :: Sing b) -> (applySing @@ -512,8 +512,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations SNil)) -> sY_0123456789876543210) sLsz - = (id - @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Nat))) + = (id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0))) (case sX_0123456789876543210 of SCons _ (SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) @@ -537,8 +536,7 @@ Singletons/PatternMatching.hs:(0,0)-(0,0): Splicing declarations -> sY_0123456789876543210) sX_0123456789876543210 = sTuple sFls - = (id - @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool))) + = (id @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0))) (case sX_0123456789876543210 of SPair (SPair _ _) (sY_0123456789876543210 :: Sing y_0123456789876543210) diff --git a/singletons-base/tests/compile-and-dump/Singletons/T150.golden b/singletons-base/tests/compile-and-dump/Singletons/T150.golden index e9848ca5..bfff42a6 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T150.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T150.golden @@ -293,7 +293,7 @@ Singletons/T150.hs:(0,0)-(0,0): Splicing declarations (%!) (SVCons _ (sXs :: Sing xs)) (SFS (sN :: Sing n)) = (applySing ((applySing ((singFun2 @(!@#@$)) (%!))) sXs)) sN (%!) SVNil (sN :: Sing n) - = (id @(Sing (Case_0123456789876543210 n n :: a))) (case sN of {}) + = (id @(Sing (Case_0123456789876543210 n n))) (case sN of {}) sTailVec (SVCons _ (sXs :: Sing xs)) = sXs sHeadVec (SVCons (sX :: Sing x) _) = sX instance SingI (TransitivitySym0 :: (~>) (Equal a b) ((~>) (Equal b c) (Equal a c))) where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T160.golden b/singletons-base/tests/compile-and-dump/Singletons/T160.golden index 046646ba..a17a7739 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T160.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T160.golden @@ -49,7 +49,7 @@ Singletons/T160.hs:(0,0)-(0,0): Splicing declarations (sFromInteger (sing :: Sing 0)) in (id - @(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) :: a))) + @(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)))) (case sScrutinee_0123456789876543210 of STrue -> sFromInteger (sing :: Sing 1) SFalse diff --git a/singletons-base/tests/compile-and-dump/Singletons/T183.golden b/singletons-base/tests/compile-and-dump/Singletons/T183.golden index 0bac4975..9f8247bd 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T183.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T183.golden @@ -423,7 +423,7 @@ Singletons/T183.hs:(0,0)-(0,0): Splicing declarations sScrutinee_0123456789876543210 = sX :: Sing (x :: Maybe a) in (id - @(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x) :: Maybe (Maybe a)))) + @(Sing (Case_0123456789876543210 x (Let0123456789876543210Scrutinee_0123456789876543210Sym1 x)))) (case sScrutinee_0123456789876543210 of SJust (sY :: Sing y) -> case ((,) (sY :: Sing y)) (SJust (sY :: Sing y)) of diff --git a/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden index f8d1b396..3e60122f 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/TopLevelPatterns.golden @@ -296,14 +296,14 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations sOtherwise :: Sing (OtherwiseSym0 :: Bool) sM = (GHC.Base.id - @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool))) + @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0))) (case sX_0123456789876543210 of SCons _ (SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) SNil) -> sY_0123456789876543210) sL = (GHC.Base.id - @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool))) + @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0))) (case sX_0123456789876543210 of SCons (sY_0123456789876543210 :: Sing y_0123456789876543210) (SCons _ SNil) @@ -318,13 +318,13 @@ Singletons/TopLevelPatterns.hs:(0,0)-(0,0): Splicing declarations SNil) sK = (GHC.Base.id - @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool))) + @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0))) (case sX_0123456789876543210 of SBar _ (sY_0123456789876543210 :: Sing y_0123456789876543210) -> sY_0123456789876543210) sJ = (GHC.Base.id - @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0 :: Bool))) + @(Sing (Case_0123456789876543210 X_0123456789876543210Sym0))) (case sX_0123456789876543210 of SBar (sY_0123456789876543210 :: Sing y_0123456789876543210) _ -> sY_0123456789876543210) diff --git a/singletons-th/src/Data/Singletons/TH/Single.hs b/singletons-th/src/Data/Singletons/TH/Single.hs index b7f00db0..e96645ca 100644 --- a/singletons-th/src/Data/Singletons/TH/Single.hs +++ b/singletons-th/src/Data/Singletons/TH/Single.hs @@ -390,10 +390,7 @@ singClassD (ClassDecl { cd_cxt = cls_cxt let default_sigs = catMaybes $ zipWith4 (mk_default_sig opts) meth_names sing_sigs tyvar_names res_kis - res_ki_map = Map.fromList (zip meth_names - (map (fromMaybe always_sig) res_kis)) - sing_meths <- mapM (uncurry (singLetDecRHS (Map.fromList cxts) - res_ki_map)) + sing_meths <- mapM (uncurry (singLetDecRHS (Map.fromList cxts))) (OMap.assocs default_defns) fixities' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs fixities cls_cxt' <- mapM singPred cls_cxt @@ -404,7 +401,6 @@ singClassD (ClassDecl { cd_cxt = cls_cxt (map DLetDec (sing_sigs ++ sing_meths ++ fixities') ++ default_sigs) where no_meth_defns = error "Internal error: can't find declared method type" - always_sig = error "Internal error: no signature for default method" meth_names = map fst $ OMap.assocs meth_sigs mk_default_sig opts meth_name (DSigD s_name sty) bound_kvs (Just res_ki) = @@ -478,35 +474,30 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys vis_cls_tvbs = drop (length cls_tvbs - length inst_kis) cls_tvbs sing_meth_ty :: OSet Name -> DType - -> SgM (DType, DCxt, DKind) + -> SgM (DType, DCxt) sing_meth_ty bound_kvs inner_ty = do -- Make sure to expand through type synonyms here! Not doing so -- resulted in #167. raw_ty <- expand inner_ty - (s_ty, _num_args, _tyvar_names, ctxt, _arg_kis, res_ki) + (s_ty, _num_args, _tyvar_names, ctxt, _arg_kis, _res_ki) <- singType bound_kvs (DConT $ defunctionalizedName0 opts name) raw_ty - pure (s_ty, ctxt, res_ki) + pure (s_ty, ctxt) - (s_ty, ctxt, m_res_ki) <- case OMap.lookup name inst_sigs of + (s_ty, ctxt) <- case OMap.lookup name inst_sigs of 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 fvDType (cxt ++ inst_kis) - (s_ty, ctxt, res_ki) <- sing_meth_ty inst_bound inst_sig - pure (s_ty, ctxt, Just res_ki) + (s_ty, ctxt) <- sing_meth_ty inst_bound inst_sig + pure (s_ty, ctxt) Nothing -> case mb_s_info of -- We don't have an InstanceSig, so we must compute the type to use -- in the singled instance ourselves through reification. Just (DVarI _ (DForallT (DForallInvis cls_tvbs) (DConstrainedT _cls_pred s_ty)) _) -> do - (_sing_tvbs, ctxt, _args, res_ty) <- unravelVanillaDType s_ty + (_sing_tvbs, ctxt, _args, _res_ty) <- unravelVanillaDType s_ty let subst = mk_subst cls_tvbs - m_res_ki = case res_ty of - _sing `DAppT` (_prom_func `DSigT` res_ki) -> Just (substKind subst res_ki) - _ -> Nothing - pure ( substType subst s_ty - , map (substType subst) ctxt - , m_res_ki ) + , map (substType subst) ctxt ) _ -> do mb_info <- dsReify name case mb_info of @@ -516,15 +507,13 @@ singInstD (InstDecl { id_cxt = cxt, id_name = inst_name, id_arg_tys = inst_tys cls_kvb_names = foldMap (foldMap fvDType . extractTvbKind) cls_tvbs cls_tvb_names = OSet.fromList $ map extractTvbName cls_tvbs cls_bound = cls_kvb_names `OSet.union` cls_tvb_names - (s_ty, ctxt, res_ki) <- sing_meth_ty cls_bound inner_ty + (s_ty, ctxt) <- sing_meth_ty cls_bound inner_ty pure ( substType subst s_ty - , ctxt - , Just (substKind subst res_ki) ) + , ctxt ) _ -> fail $ "Cannot find type of method " ++ show name - let kind_map = maybe Map.empty (Map.singleton name) m_res_ki meth' <- singLetDecRHS (Map.singleton name ctxt) - kind_map name rhs + name rhs return $ map DLetDec [DSigD (singledValueName opts name) s_ty, meth'] singLetDecEnv :: ALetDecEnv @@ -543,14 +532,11 @@ singLetDecEnv (LetDecEnv { lde_defns = defns , lde_bound_kvs = bound_kvs }) thing_inside = do let prom_list = OMap.assocs proms - (typeSigs, letBinds, _tyvarNames, cxts, res_kis, singIDefunss) + (typeSigs, letBinds, _tyvarNames, cxts, _res_kis, singIDefunss) <- unzip6 <$> mapM (uncurry (singTySig defns types bound_kvs)) prom_list infix_decls' <- mapMaybeM (uncurry singInfixDecl) $ OMap.assocs infix_decls - let res_ki_map = Map.fromList [ (name, res_ki) | ((name, _), Just res_ki) - <- zip prom_list res_kis ] bindLets letBinds $ do - let_decs <- mapM (uncurry (singLetDecRHS (Map.fromList cxts) - res_ki_map)) + let_decs <- mapM (uncurry (singLetDecRHS (Map.fromList cxts))) (OMap.assocs defns) thing <- thing_inside return (infix_decls' ++ typeSigs ++ let_decs, concat singIDefunss, thing) @@ -722,26 +708,22 @@ above. singLetDecRHS :: Map Name DCxt -- the context of the type signature -- (might not be known) - -> Map Name DKind -- result kind (might not be known) -> Name -> ALetDecRHS -> SgM DLetDec -singLetDecRHS cxts res_kis name ld_rhs = do +singLetDecRHS cxts name ld_rhs = do opts <- getOptions bindContext (Map.findWithDefault [] name cxts) $ case ld_rhs of AValue exp -> DValD (DVarP (singledValueName opts name)) <$> - singExp exp (Map.lookup name res_kis) + singExp exp AFunction _num_arrows clauses -> - let res_ki = Map.lookup name res_kis - in DFunD (singledValueName opts name) <$> - mapM (singClause res_ki) clauses + mapM singClause clauses -singClause :: Maybe DKind -- result kind, if known - -> ADClause -> SgM DClause -singClause res_ki (ADClause var_proms pats exp) = do +singClause :: ADClause -> SgM DClause +singClause (ADClause var_proms pats exp) = do (sPats, sigPaExpsSigs) <- evalForPair $ mapM (singPat (Map.fromList var_proms)) pats - sBody <- singExp exp res_ki + sBody <- singExp exp return $ DClause sPats $ mkSigPaCaseE sigPaExpsSigs sBody singPat :: Map Name Name -- from term-level names to type-level names @@ -897,28 +879,27 @@ mkSigPaCaseE exps_with_sigs exp -- -- And now everything is hunky-dory. -singExp :: ADExp -> Maybe DKind -- the kind of the expression, if known - -> SgM DExp +singExp :: ADExp -> SgM DExp -- See Note [Why error is so special] -singExp (ADVarE err `ADAppE` arg) _res_ki +singExp (ADVarE err `ADAppE` arg) | err == errorName = do opts <- getOptions DAppE (DVarE (singledValueName opts err)) <$> - singExp arg (Just (DConT symbolName)) -singExp (ADVarE name) _res_ki = lookupVarE name -singExp (ADConE name) _res_ki = lookupConE name -singExp (ADLitE lit) _res_ki = singLit lit -singExp (ADAppE e1 e2) _res_ki = do - e1' <- singExp e1 Nothing - e2' <- singExp e2 Nothing + singExp arg +singExp (ADVarE name) = lookupVarE name +singExp (ADConE name) = lookupConE name +singExp (ADLitE lit) = singLit lit +singExp (ADAppE e1 e2) = do + e1' <- singExp e1 + e2' <- singExp e2 -- `applySing undefined x` kills type inference, because GHC can't figure -- out the type of `undefined`. So we don't emit `applySing` there. if isException e1' then return $ e1' `DAppE` e2' else return $ (DVarE applySingName) `DAppE` e1' `DAppE` e2' -singExp (ADLamE ty_names prom_lam names exp) _res_ki = do +singExp (ADLamE ty_names prom_lam names exp) = do opts <- getOptions let sNames = map (singledValueName opts) names - exp' <- singExp exp Nothing + exp' <- singExp exp -- we need to bind the type variables... but DLamE doesn't allow SigT patterns. -- So: build a case let caseExp = DCaseE (mkTupleDExp (map DVarE sNames)) @@ -927,21 +908,21 @@ singExp (ADLamE ty_names prom_lam names exp) _res_ki = do (singFamily `DAppT`) . DVarT) ty_names)) exp'] return $ wrapSingFun (length names) prom_lam $ DLamE sNames caseExp -singExp (ADCaseE exp matches ret_ty) res_ki = +singExp (ADCaseE exp matches ret_ty) = -- See Note [Annotate case return type] and -- Note [The id hack; or, how singletons-th learned to stop worrying and -- avoid kind generalization] DAppE (DAppTypeE (DVarE 'id) - (singFamily `DAppT` (ret_ty `maybeSigT` res_ki))) - <$> (DCaseE <$> singExp exp Nothing <*> mapM (singMatch res_ki) matches) -singExp (ADLetE env exp) res_ki = do + (singFamily `DAppT` ret_ty)) + <$> (DCaseE <$> singExp exp <*> mapM singMatch matches) +singExp (ADLetE env exp) = do -- We intentionally discard the SingI instances for exp's defunctionalization -- symbols, as we also do not generate the declarations for the -- defunctionalization symbols in the first place during promotion. - (let_decs, _, exp') <- singLetDecEnv env $ singExp exp res_ki + (let_decs, _, exp') <- singLetDecEnv env $ singExp exp pure $ DLetE let_decs exp' -singExp (ADSigE prom_exp exp ty) _ = do - exp' <- singExp exp (Just ty) +singExp (ADSigE prom_exp exp ty) = do + exp' <- singExp exp pure $ DSigE exp' $ DConT singFamilyName `DAppT` DSigT prom_exp ty -- See Note [DerivedDecl] in Data.Singletons.TH.Syntax @@ -1011,11 +992,10 @@ isException (DLetE _ e) = isException e isException (DSigE e _) = isException e isException (DStaticE e) = isException e -singMatch :: Maybe DKind -- ^ the result kind, if known - -> ADMatch -> SgM DMatch -singMatch res_ki (ADMatch var_proms pat exp) = do +singMatch :: ADMatch -> SgM DMatch +singMatch (ADMatch var_proms pat exp) = do (sPat, sigPaExpsSigs) <- evalForPair $ singPat (Map.fromList var_proms) pat - sExp <- singExp exp res_ki + sExp <- singExp exp return $ DMatch sPat $ mkSigPaCaseE sigPaExpsSigs sExp singLit :: Lit -> SgM DExp diff --git a/singletons-th/src/Data/Singletons/TH/Single/Type.hs b/singletons-th/src/Data/Singletons/TH/Single/Type.hs index c923962b..c8260fe6 100644 --- a/singletons-th/src/Data/Singletons/TH/Single/Type.hs +++ b/singletons-th/src/Data/Singletons/TH/Single/Type.hs @@ -151,33 +151,15 @@ What happens if there is no explicit `forall`, as in this example? absurd v = case v of {} This time, the order of type variables vis-à-vis TypeApplications is determined -by their left-to-right order of appearance in the type signature. It's tempting -to think that since there is no explicit `forall` in the original type -signature, we could get away without an explicit `forall` in the singled type -signature. That is, one could write: +by their left-to-right order of appearance in the type signature. This order +dictates that `a` is quantified before `b`, so we mirror this order in the +singled type signature: - sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b) + sAbsurd :: forall a b (v :: V a). Sing v -> Sing (Absurd v :: b) -This would have the right type variable order, but unfortunately, this approach -does not play well with singletons-th's style of code generation. Consider the code -that would be generated for the body of sAbsurd: - - sAbsurd :: Sing (v :: V a) -> Sing (Absurd :: b) - sAbsurd (sV :: Sing v) = id @(Case v v :: b) (case sV of {}) - -Note the use of the type `Case v v :: b` in the right-hand side of sAbsurd. -However, because `b` was not bound by a top-level `forall`, it won't be in -scope here, resulting in an error! - -(Why do we generate the code `id @(Case v v :: b)` in the first place? See -Note [The id hack; or, how singletons-th learned to stop worrying and avoid kind generalization] -in D.S.TH.Single.) - -The simplest approach is to just always generate singled type signatures with -explicit `forall`s. In the event that the original type signature lacks an -explicit `forall`, we infer the correct type variable ordering ourselves and -synthesize a `forall` with that order. The `singTypeKVBs` function implements -this logic. +The `singTypeKVBs` function is responsible for detecting the presence or +absence of an explicit `forall`, and in the event that an explicit `forall` is +omitted, it infers the correct order of type variables. ----- -- Wrinkle 2: The TH reification swamp