From 1668618b30d6b50ee774864500ac0a814c6aa1ce Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sun, 30 Jun 2024 16:58:25 -0400 Subject: [PATCH] Give helper type families more precise kinds When promoting a class or instance method, we generate a "helper" type family definition that contains the actual implementation of the class or instance method. Prior to this patch, it was possible that the kind of the helper type family could be more polymorphic than desired. For instance, `singletons-th` would promote this: ```hs $(promote [d| type MyApplicative :: (Type -> Type) -> Constraint class Functor f => MyApplicative f where ap :: f (a -> b) -> f a -> f b rightSparrow :: f a -> f b -> f b rightSparrow x y = ap (id <$ x) y |]) ``` To this: ```hs type PMyApplicative :: (Type -> Type) -> Constraint class PMyApplicative f where type Ap (x :: f (a ~> b)) (y :: f a) :: f b type RightSparrow (x :: f a) (y :: f b) :: f b type RightSparrow x y = RightSparrowDefault x y -- The helper type family type RightSparrowDefault :: forall f a b. f a -> f b -> f b type family RightSparrowDefault x y where RightSparrowDefault x y = Ap (IdSym0 <$ x) y ``` Note that GHC would generalize the standalone kind signature of `RightSparrowDefault` to: ```hs type RightSparrowDefault :: forall {k} (f :: k -> Type) (a :: k) (b :: k). f a -> f b -> f b ``` This is more general than intended, as we want `f` to be of kind `Type -> Type` instead. After all, we said as much in the standalone kind signature for `MyApplicative`! This excessive polymorphism doesn't actively cause problems in today's GHC, but they will cause problems in a future version of GHC that implements [GHC#23515](https://gitlab.haskell.org/ghc/ghc/-/issues/23515). (See #601.) This patch resolves the issue by propagating kind information from the class's standalone kind signature (or, in the case of instance declarations, the instance head) to the helper type family declarations. After this patch, we now generate the following kind for `RightSparrowDefault` (as verified by the new `T601a` test case): ```hs type RightSparrowDefault :: forall (f :: Type -> Type) a b. f a -> f b -> f b ``` This piggybacks on machinery that was added in #596 to do most of the heavy lifting. Resolves the "Overly polymorphic promoted class defaults" section of #601. --- .../tests/SingletonsBaseTestSuite.hs | 1 + .../compile-and-dump/Promote/T601a.golden | 73 +++++++++ .../tests/compile-and-dump/Promote/T601a.hs | 14 ++ .../Singletons/FunctorLikeDeriving.golden | 40 ++--- .../compile-and-dump/Singletons/T358.golden | 12 +- .../compile-and-dump/Singletons/T581.golden | 18 +- .../src/Data/Singletons/TH/Promote.hs | 154 ++++++++++++------ 7 files changed, 229 insertions(+), 83 deletions(-) create mode 100644 singletons-base/tests/compile-and-dump/Promote/T601a.golden create mode 100644 singletons-base/tests/compile-and-dump/Promote/T601a.hs diff --git a/singletons-base/tests/SingletonsBaseTestSuite.hs b/singletons-base/tests/SingletonsBaseTestSuite.hs index 8698b7c3..cce4299f 100644 --- a/singletons-base/tests/SingletonsBaseTestSuite.hs +++ b/singletons-base/tests/SingletonsBaseTestSuite.hs @@ -166,6 +166,7 @@ tests = , compileAndDumpStdTest "Prelude" , compileAndDumpStdTest "T180" , compileAndDumpStdTest "T361" + , compileAndDumpStdTest "T601a" , compileAndDumpStdTest "T605" ], testGroup "Database client" diff --git a/singletons-base/tests/compile-and-dump/Promote/T601a.golden b/singletons-base/tests/compile-and-dump/Promote/T601a.golden new file mode 100644 index 00000000..98b7ecfa --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Promote/T601a.golden @@ -0,0 +1,73 @@ +Promote/T601a.hs:(0,0)-(0,0): Splicing declarations + promote + [d| type MyApplicative :: (Type -> Type) -> Constraint + + class Functor f => MyApplicative f where + ap :: f (a -> b) -> f a -> f b + rightSparrow :: f a -> f b -> f b + rightSparrow x y = ap (id <$ x) y |] + ======> + type MyApplicative :: (Type -> Type) -> Constraint + class Functor f => MyApplicative f where + ap :: f (a -> b) -> f a -> f b + rightSparrow :: f a -> f b -> f b + rightSparrow x y = ap (id <$ x) y + type ApSym0 :: forall (f :: Type -> Type) + a + b. (~>) (f ((~>) a b)) ((~>) (f a) (f b)) + data ApSym0 :: (~>) (f ((~>) a b)) ((~>) (f a) (f b)) + where + ApSym0KindInference :: SameKind (Apply ApSym0 arg) (ApSym1 arg) => + ApSym0 a0123456789876543210 + type instance Apply @(f ((~>) a b)) @((~>) (f a) (f b)) ApSym0 a0123456789876543210 = ApSym1 a0123456789876543210 + instance SuppressUnusedWarnings ApSym0 where + suppressUnusedWarnings = snd ((,) ApSym0KindInference ()) + type ApSym1 :: forall (f :: Type -> Type) a b. f ((~>) a b) + -> (~>) (f a) (f b) + data ApSym1 (a0123456789876543210 :: f ((~>) a b)) :: (~>) (f a) (f b) + where + ApSym1KindInference :: SameKind (Apply (ApSym1 a0123456789876543210) arg) (ApSym2 a0123456789876543210 arg) => + ApSym1 a0123456789876543210 a0123456789876543210 + type instance Apply @(f a) @(f b) (ApSym1 a0123456789876543210) a0123456789876543210 = Ap a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (ApSym1 a0123456789876543210) where + suppressUnusedWarnings = snd ((,) ApSym1KindInference ()) + type ApSym2 :: forall (f :: Type -> Type) a b. f ((~>) a b) + -> f a -> f b + type family ApSym2 @(f :: Type + -> Type) @a @b (a0123456789876543210 :: f ((~>) a b)) (a0123456789876543210 :: f a) :: f b where + ApSym2 a0123456789876543210 a0123456789876543210 = Ap a0123456789876543210 a0123456789876543210 + type RightSparrowSym0 :: forall (f :: Type -> Type) + a + b. (~>) (f a) ((~>) (f b) (f b)) + data RightSparrowSym0 :: (~>) (f a) ((~>) (f b) (f b)) + where + RightSparrowSym0KindInference :: SameKind (Apply RightSparrowSym0 arg) (RightSparrowSym1 arg) => + RightSparrowSym0 a0123456789876543210 + type instance Apply @(f a) @((~>) (f b) (f b)) RightSparrowSym0 a0123456789876543210 = RightSparrowSym1 a0123456789876543210 + instance SuppressUnusedWarnings RightSparrowSym0 where + suppressUnusedWarnings = snd ((,) RightSparrowSym0KindInference ()) + type RightSparrowSym1 :: forall (f :: Type -> Type) a b. f a + -> (~>) (f b) (f b) + data RightSparrowSym1 (a0123456789876543210 :: f a) :: (~>) (f b) (f b) + where + RightSparrowSym1KindInference :: SameKind (Apply (RightSparrowSym1 a0123456789876543210) arg) (RightSparrowSym2 a0123456789876543210 arg) => + RightSparrowSym1 a0123456789876543210 a0123456789876543210 + type instance Apply @(f b) @(f b) (RightSparrowSym1 a0123456789876543210) a0123456789876543210 = RightSparrow a0123456789876543210 a0123456789876543210 + instance SuppressUnusedWarnings (RightSparrowSym1 a0123456789876543210) where + suppressUnusedWarnings = snd ((,) RightSparrowSym1KindInference ()) + type RightSparrowSym2 :: forall (f :: Type -> Type) a b. f a + -> f b -> f b + type family RightSparrowSym2 @(f :: Type + -> Type) @a @b (a0123456789876543210 :: f a) (a0123456789876543210 :: f b) :: f b where + RightSparrowSym2 a0123456789876543210 a0123456789876543210 = RightSparrow a0123456789876543210 a0123456789876543210 + type RightSparrow_0123456789876543210 :: forall (f :: Type -> Type) + a + b. f a -> f b -> f b + type family RightSparrow_0123456789876543210 @(f :: Type + -> Type) @a @b (a :: f a) (a :: f b) :: f b where + RightSparrow_0123456789876543210 @f @a @b (x :: f a) (y :: f b) = Apply (Apply ApSym0 (Apply (Apply (<$@#@$) IdSym0) x)) y + type PMyApplicative :: (Type -> Type) -> Constraint + class PMyApplicative f where + type family Ap (arg :: f ((~>) a b)) (arg :: f a) :: f b + type family RightSparrow (arg :: f a) (arg :: f b) :: f b + type RightSparrow a a = RightSparrow_0123456789876543210 a a diff --git a/singletons-base/tests/compile-and-dump/Promote/T601a.hs b/singletons-base/tests/compile-and-dump/Promote/T601a.hs new file mode 100644 index 00000000..ff182e10 --- /dev/null +++ b/singletons-base/tests/compile-and-dump/Promote/T601a.hs @@ -0,0 +1,14 @@ +module T601a where + +import Data.Kind +import Data.Singletons.Base.TH +import Prelude.Singletons + +$(promote [d| + type MyApplicative :: (Type -> Type) -> Constraint + class Functor f => MyApplicative f where + ap :: f (a -> b) -> f a -> f b + + rightSparrow :: f a -> f b -> f b + rightSparrow x y = ap (id <$ x) y + |]) diff --git a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden index ef939b44..b6b4ceb3 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/FunctorLikeDeriving.golden @@ -84,11 +84,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) LamCases_0123456789876543210Sym0KindInference ()) type family LamCases_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 where LamCases_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 - type Fmap_0123456789876543210 :: forall a b x. (~>) a b + type Fmap_0123456789876543210 :: forall x a b. (~>) a b -> T x a -> T x b - type family Fmap_0123456789876543210 @a @b @x (a :: (~>) a b) (a :: T x a) :: T x b where - Fmap_0123456789876543210 @a @b @x (_f_0123456789876543210 :: (~>) a b) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply (Apply (Apply MkT1Sym0 (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply FmapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FmapSym0 (Apply FmapSym0 _f_0123456789876543210)) a_0123456789876543210) - Fmap_0123456789876543210 @a @b @x (_f_0123456789876543210 :: (~>) a b) (MkT2 a_0123456789876543210 :: T x a) = Apply MkT2Sym0 (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210) a_0123456789876543210) + type family Fmap_0123456789876543210 @x @a @b (a :: (~>) a b) (a :: T x a) :: T x b where + Fmap_0123456789876543210 @x @a @b (_f_0123456789876543210 :: (~>) a b) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply (Apply (Apply MkT1Sym0 (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply FmapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FmapSym0 (Apply FmapSym0 _f_0123456789876543210)) a_0123456789876543210) + Fmap_0123456789876543210 @x @a @b (_f_0123456789876543210 :: (~>) a b) (MkT2 a_0123456789876543210 :: T x a) = Apply MkT2Sym0 (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210) a_0123456789876543210) type family LamCases_0123456789876543210 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_0123456789876543210 where LamCases_0123456789876543210 x _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 n_0123456789876543210 = n_0123456789876543210 data LamCases_0123456789876543210Sym0 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 @@ -125,11 +125,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) LamCases_0123456789876543210Sym0KindInference ()) type family LamCases_0123456789876543210Sym1 x0123456789876543210 (_z_01234567898765432100123456789876543210 :: a0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 where LamCases_0123456789876543210Sym1 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 - type TFHelper_0123456789876543210 :: forall a x b. a + type TFHelper_0123456789876543210 :: forall x a b. a -> T x b -> T x a - type family TFHelper_0123456789876543210 @a @x @b (a :: a) (a :: T x b) :: T x a where - TFHelper_0123456789876543210 @a @x @b (_z_0123456789876543210 :: a) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x b) = Apply (Apply (Apply (Apply MkT1Sym0 (Apply (LamCases_0123456789876543210Sym0 x _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply (LamCases_0123456789876543210Sym0 x _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply (Apply (<$@#@$) _z_0123456789876543210) a_0123456789876543210)) (Apply (Apply FmapSym0 (Apply (<$@#@$) _z_0123456789876543210)) a_0123456789876543210) - TFHelper_0123456789876543210 @a @x @b (_z_0123456789876543210 :: a) (MkT2 a_0123456789876543210 :: T x b) = Apply MkT2Sym0 (Apply (LamCases_0123456789876543210Sym0 x _z_0123456789876543210 a_0123456789876543210) a_0123456789876543210) + type family TFHelper_0123456789876543210 @x @a @b (a :: a) (a :: T x b) :: T x a where + TFHelper_0123456789876543210 @x @a @b (_z_0123456789876543210 :: a) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x b) = Apply (Apply (Apply (Apply MkT1Sym0 (Apply (LamCases_0123456789876543210Sym0 x _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply (LamCases_0123456789876543210Sym0 x _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply (Apply (<$@#@$) _z_0123456789876543210) a_0123456789876543210)) (Apply (Apply FmapSym0 (Apply (<$@#@$) _z_0123456789876543210)) a_0123456789876543210) + TFHelper_0123456789876543210 @x @a @b (_z_0123456789876543210 :: a) (MkT2 a_0123456789876543210 :: T x b) = Apply MkT2Sym0 (Apply (LamCases_0123456789876543210Sym0 x _z_0123456789876543210 a_0123456789876543210) a_0123456789876543210) instance PFunctor (T x) where type Fmap a a = Fmap_0123456789876543210 a a type (<$) a a = TFHelper_0123456789876543210 a a @@ -157,11 +157,11 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) LamCases_0123456789876543210Sym0KindInference ()) type family LamCases_0123456789876543210Sym1 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 m0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 where LamCases_0123456789876543210Sym1 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 - type FoldMap_0123456789876543210 :: forall a m x. (~>) a m + type FoldMap_0123456789876543210 :: forall x a m. (~>) a m -> T x a -> m - type family FoldMap_0123456789876543210 @a @m @x (a :: (~>) a m) (a :: T x a) :: m where - FoldMap_0123456789876543210 @a @m @x (_f_0123456789876543210 :: (~>) a m) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply MappendSym0 (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply (Apply FoldMapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FoldMapSym0 (Apply FoldMapSym0 _f_0123456789876543210)) a_0123456789876543210))) - FoldMap_0123456789876543210 @a @m @x (_f_0123456789876543210 :: (~>) a m) (MkT2 a_0123456789876543210 :: T x a) = Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210) a_0123456789876543210 + type family FoldMap_0123456789876543210 @x @a @m (a :: (~>) a m) (a :: T x a) :: m where + FoldMap_0123456789876543210 @x @a @m (_f_0123456789876543210 :: (~>) a m) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply MappendSym0 (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply _f_0123456789876543210 a_0123456789876543210)) (Apply (Apply MappendSym0 (Apply (Apply FoldMapSym0 _f_0123456789876543210) a_0123456789876543210)) (Apply (Apply FoldMapSym0 (Apply FoldMapSym0 _f_0123456789876543210)) a_0123456789876543210))) + FoldMap_0123456789876543210 @x @a @m (_f_0123456789876543210 :: (~>) a m) (MkT2 a_0123456789876543210 :: T x a) = Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 a_0123456789876543210) a_0123456789876543210 type family LamCases_0123456789876543210 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_0123456789876543210 a_0123456789876543210 where LamCases_0123456789876543210 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 _ n_0123456789876543210 = n_0123456789876543210 data LamCases_0123456789876543210Sym0 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 @@ -262,19 +262,19 @@ Singletons/FunctorLikeDeriving.hs:(0,0)-(0,0): Splicing declarations = snd ((,) LamCases_0123456789876543210Sym1KindInference ()) type family LamCases_0123456789876543210Sym2 x0123456789876543210 (_f_01234567898765432100123456789876543210 :: (~>) a0123456789876543210 ((~>) b0123456789876543210 b0123456789876543210)) (_z_01234567898765432100123456789876543210 :: b0123456789876543210) a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 where LamCases_0123456789876543210Sym2 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 = LamCases_0123456789876543210 x0123456789876543210 _f_01234567898765432100123456789876543210 _z_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 a_01234567898765432100123456789876543210 - type Foldr_0123456789876543210 :: forall a b x. (~>) a ((~>) b b) + type Foldr_0123456789876543210 :: forall x a b. (~>) a ((~>) b b) -> b -> T x a -> b - type family Foldr_0123456789876543210 @a @b @x (a :: (~>) a ((~>) b b)) (a :: b) (a :: T x a) :: b where - Foldr_0123456789876543210 @a @b @x (_f_0123456789876543210 :: (~>) a ((~>) b b)) (_z_0123456789876543210 :: b) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) (Apply (Apply _f_0123456789876543210 a_0123456789876543210) (Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) (Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) _z_0123456789876543210))) - Foldr_0123456789876543210 @a @b @x (_f_0123456789876543210 :: (~>) a ((~>) b b)) (_z_0123456789876543210 :: b) (MkT2 a_0123456789876543210 :: T x a) = Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210) a_0123456789876543210) _z_0123456789876543210 + type family Foldr_0123456789876543210 @x @a @b (a :: (~>) a ((~>) b b)) (a :: b) (a :: T x a) :: b where + Foldr_0123456789876543210 @x @a @b (_f_0123456789876543210 :: (~>) a ((~>) b b)) (_z_0123456789876543210 :: b) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) (Apply (Apply _f_0123456789876543210 a_0123456789876543210) (Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) (Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210) a_0123456789876543210) _z_0123456789876543210))) + Foldr_0123456789876543210 @x @a @b (_f_0123456789876543210 :: (~>) a ((~>) b b)) (_z_0123456789876543210 :: b) (MkT2 a_0123456789876543210 :: T x a) = Apply (Apply (LamCases_0123456789876543210Sym0 x _f_0123456789876543210 _z_0123456789876543210 a_0123456789876543210) a_0123456789876543210) _z_0123456789876543210 instance PFoldable (T x) where type FoldMap a a = FoldMap_0123456789876543210 a a type Foldr a a a = Foldr_0123456789876543210 a a a - type Traverse_0123456789876543210 :: forall a f b x. (~>) a (f b) + type Traverse_0123456789876543210 :: forall x a f b. (~>) a (f b) -> T x a -> f (T x b) - type family Traverse_0123456789876543210 @a @f @b @x (a :: (~>) a (f b)) (a :: T x a) :: f (T x b) where - Traverse_0123456789876543210 @a @f @b @x (_f_0123456789876543210 :: (~>) a (f b)) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply (<*>@#@$) (Apply (Apply (<*>@#@$) (Apply (Apply (Apply LiftA2Sym0 MkT1Sym0) (Apply PureSym0 a_0123456789876543210)) (Apply _f_0123456789876543210 a_0123456789876543210))) (Apply (Apply TraverseSym0 _f_0123456789876543210) a_0123456789876543210))) (Apply (Apply TraverseSym0 (Apply TraverseSym0 _f_0123456789876543210)) a_0123456789876543210) - Traverse_0123456789876543210 @a @f @b @x (_f_0123456789876543210 :: (~>) a (f b)) (MkT2 a_0123456789876543210 :: T x a) = Apply (Apply FmapSym0 MkT2Sym0) (Apply PureSym0 a_0123456789876543210) + type family Traverse_0123456789876543210 @x @a @f @b (a :: (~>) a (f b)) (a :: T x a) :: f (T x b) where + Traverse_0123456789876543210 @x @a @f @b (_f_0123456789876543210 :: (~>) a (f b)) (MkT1 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 a_0123456789876543210 :: T x a) = Apply (Apply (<*>@#@$) (Apply (Apply (<*>@#@$) (Apply (Apply (Apply LiftA2Sym0 MkT1Sym0) (Apply PureSym0 a_0123456789876543210)) (Apply _f_0123456789876543210 a_0123456789876543210))) (Apply (Apply TraverseSym0 _f_0123456789876543210) a_0123456789876543210))) (Apply (Apply TraverseSym0 (Apply TraverseSym0 _f_0123456789876543210)) a_0123456789876543210) + Traverse_0123456789876543210 @x @a @f @b (_f_0123456789876543210 :: (~>) a (f b)) (MkT2 a_0123456789876543210 :: T x a) = Apply (Apply FmapSym0 MkT2Sym0) (Apply PureSym0 a_0123456789876543210) instance PTraversable (T x) where type Traverse a a = Traverse_0123456789876543210 a a type family LamCases_0123456789876543210 (v_01234567898765432100123456789876543210 :: Empty a0123456789876543210) a_0123456789876543210 where diff --git a/singletons-base/tests/compile-and-dump/Singletons/T358.golden b/singletons-base/tests/compile-and-dump/Singletons/T358.golden index 3814622b..08a2a25e 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T358.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T358.golden @@ -60,12 +60,12 @@ Singletons/T358.hs:(0,0)-(0,0): Splicing declarations Method1_0123456789876543210 @a = NilSym0 instance PC1 [] where type Method1 = Method1_0123456789876543210 - type Method2a_0123456789876543210 :: forall b a. b -> [a] - type family Method2a_0123456789876543210 @b @a (a :: b) :: [a] where - Method2a_0123456789876543210 @b @a (_ :: b) = NilSym0 - type Method2b_0123456789876543210 :: forall b a. b -> [a] - type family Method2b_0123456789876543210 @b @a (a :: b) :: [a] where - Method2b_0123456789876543210 @b @a (_ :: b) = NilSym0 + type Method2a_0123456789876543210 :: forall a b. b -> [a] + type family Method2a_0123456789876543210 @a @b (a :: b) :: [a] where + Method2a_0123456789876543210 @a @b (_ :: b) = NilSym0 + type Method2b_0123456789876543210 :: forall a b. b -> [a] + type family Method2b_0123456789876543210 @a @b (a :: b) :: [a] where + Method2b_0123456789876543210 @a @b (_ :: b) = NilSym0 instance PC2 [a] where type Method2a a = Method2a_0123456789876543210 a type Method2b a = Method2b_0123456789876543210 a diff --git a/singletons-base/tests/compile-and-dump/Singletons/T581.golden b/singletons-base/tests/compile-and-dump/Singletons/T581.golden index d9b5cf8f..c1b3a86b 100644 --- a/singletons-base/tests/compile-and-dump/Singletons/T581.golden +++ b/singletons-base/tests/compile-and-dump/Singletons/T581.golden @@ -77,9 +77,9 @@ Singletons/T581.hs:(0,0)-(0,0): Splicing declarations type M2Sym1 :: forall b a. b -> Maybe a type family M2Sym1 @b @a (a0123456789876543210 :: b) :: Maybe a where M2Sym1 a0123456789876543210 = M2 a0123456789876543210 - type M2_0123456789876543210 :: forall b a. b -> Maybe a - type family M2_0123456789876543210 @b @a (a :: b) :: Maybe a where - M2_0123456789876543210 @b @a (_ :: b) = NothingSym0 :: Maybe a + type M2_0123456789876543210 :: forall a b. b -> Maybe a + type family M2_0123456789876543210 @a @b (a :: b) :: Maybe a where + M2_0123456789876543210 @a @b (_ :: b) = NothingSym0 :: Maybe a class PC2 a where type family M2 (arg :: b) :: Maybe a type M2 a = M2_0123456789876543210 a @@ -120,14 +120,14 @@ Singletons/T581.hs:(0,0)-(0,0): Splicing declarations b) instance PC1 [a] where type M1 a = M1_0123456789876543210 a - type M2_0123456789876543210 :: forall b a. b -> Maybe [a] - type family M2_0123456789876543210 @b @a (a :: b) :: Maybe [a] where - M2_0123456789876543210 @b @a (_ :: b) = NothingSym0 :: Maybe [a] + type M2_0123456789876543210 :: forall a b. b -> Maybe [a] + type family M2_0123456789876543210 @a @b (a :: b) :: Maybe [a] where + M2_0123456789876543210 @a @b (_ :: b) = NothingSym0 :: Maybe [a] instance PC2 [a] where type M2 a = M2_0123456789876543210 a - type M2_0123456789876543210 :: forall b a. b -> Maybe (Maybe a) - type family M2_0123456789876543210 @b @a (a :: b) :: Maybe (Maybe a) where - M2_0123456789876543210 @b @a (_ :: b) = NothingSym0 :: Maybe (Maybe a) + type M2_0123456789876543210 :: forall a b. b -> Maybe (Maybe a) + type family M2_0123456789876543210 @a @b (a :: b) :: Maybe (Maybe a) where + M2_0123456789876543210 @a @b (_ :: b) = NothingSym0 :: Maybe (Maybe a) instance PC2 (Maybe a) where type M2 a = M2_0123456789876543210 a type family LamCases_0123456789876543210 a0123456789876543210 (x0123456789876543210 :: Maybe a0123456789876543210) (y0123456789876543210 :: b0123456789876543210) a_0123456789876543210 where diff --git a/singletons-th/src/Data/Singletons/TH/Promote.hs b/singletons-th/src/Data/Singletons/TH/Promote.hs index 8bd8f779..77fc1549 100644 --- a/singletons-th/src/Data/Singletons/TH/Promote.hs +++ b/singletons-th/src/Data/Singletons/TH/Promote.hs @@ -278,7 +278,6 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name meth_names = map fst meth_sigs_list defaults_list = OMap.assocs defaults defaults_names = map fst defaults_list - cls_tvb_names = map extractTvbName orig_cls_tvbs mb_cls_sak <- dsReifyType cls_name -- If the class has a standalone kind signature, we take the original, @@ -287,10 +286,19 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name -- Note [Propagating kind information from class standalone kind signatures]. mb_full_cls_tvbs <- traverse (\cls_sak -> matchUpSAKWithDecl cls_sak orig_cls_tvbs) mb_cls_sak - - sig_decs <- mapM (uncurry (promote_sig mb_full_cls_tvbs)) meth_sigs_list + let mb_full_cls_tvbs_spec = tvbForAllTyFlagsToSpecs <$> mb_full_cls_tvbs + -- The class binders, converted to `DTyVarBndrSpec`s. If the parent class + -- has a standalone kind signature, we compute these `DTyVarBndrSpec`s + -- from the full class binders, which likely have richer kind information. + -- Otherwise, we compute these from the original, user-written class + -- binders. + cls_tvbs_spec = fromMaybe + (changeDTVFlags SpecifiedSpec orig_cls_tvbs) + mb_full_cls_tvbs_spec + + sig_decs <- mapM (uncurry (promote_sig mb_full_cls_tvbs_spec)) meth_sigs_list (default_decs, ann_rhss, prom_rhss) - <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs cls_tvb_names) defaults_list + <- mapAndUnzip3M (promoteMethod DefaultMethods meth_sigs cls_tvbs_spec) defaults_list defunAssociatedTypeFamilies orig_cls_tvbs atfs infix_decls' <- mapMaybeM (\(n, (f, ns)) -> promoteInfixDecl Nothing n f ns) $ @@ -309,7 +317,7 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name where -- Promote a class method's type signature to an associated type family. promote_sig :: - Maybe [DTyVarBndr ForAllTyFlag] + Maybe [DTyVarBndrSpec] -- ^ If the parent class has a standalone kind signature, then this -- will be @'Just' full_bndrs@, where @full_bndrs@ are the full type -- variable binders described in @Note [Propagating kind information @@ -321,7 +329,7 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name -- ^ The class method's type. -> PrM DDec -- ^ The associated type family for the promoted class method. - promote_sig mb_full_cls_tvbs name meth_ty = do + promote_sig mb_full_cls_tvbs_spec name meth_ty = do opts <- getOptions let proName = promotedTopLevelValueName opts name (_, meth_arg_kis, meth_res_ki) <- promoteUnraveled meth_ty @@ -340,7 +348,7 @@ promoteClassDec decl@(ClassDecl { cd_name = cls_name -- The type variable binders to use in the standalone kind signatures -- for the promoted class method's defunctionalization symbols. meth_sak_tvbs = - case tvbForAllTyFlagsToSpecs <$> mb_full_cls_tvbs of + case mb_full_cls_tvbs_spec of -- If the parent class has a standalone kind signature, then -- propagate as much of the kind information as possible by -- incorporating the full class binders. See Note [Propagating @@ -546,9 +554,9 @@ promoteInstanceDec orig_meth_sigs cls_tvbs_map cls_tvb_names = map extractTvbName cls_tvbs subst = Map.fromList $ zip cls_tvb_names inst_kis meth_impl = InstanceMethods inst_sigs subst - inst_ki_fvs = map extractTvbName $ toposortTyVarsOf inst_kis + inst_ki_kvbs = changeDTVFlags SpecifiedSpec $ toposortTyVarsOf inst_kis (meths', ann_rhss, _) - <- mapAndUnzip3M (promoteMethod meth_impl orig_meth_sigs inst_ki_fvs) meths + <- mapAndUnzip3M (promoteMethod meth_impl orig_meth_sigs inst_ki_kvbs) meths emitDecs [DInstanceD Nothing Nothing [] (foldType (DConT pClsName) inst_kis) meths'] return (decl { id_meths = zip (map fst meths) ann_rhss }) @@ -630,14 +638,15 @@ data MethodSort promoteMethod :: MethodSort -> OMap Name DType -- method types - -> [Name] -- The names of the type variables bound by the class - -- header (e.g., the @a@ in @class C a where ...@). + -> [DTyVarBndrSpec] -- The type variables bound by the class + -- header (e.g., the @a b@ in + -- @class C a b where ...@). -> (Name, ULetDecRHS) -> PrM (DDec, ALetDecRHS, LetDecProm) -- returns (type instance, ALetDecRHS, promoted RHS) -promoteMethod meth_sort orig_sigs_map cls_tvb_names (meth_name, meth_rhs) = do +promoteMethod meth_sort orig_sigs_map cls_tvbs (meth_name, meth_rhs) = do opts <- getOptions - (meth_tvbs, meth_arg_kis, meth_res_ki) <- promote_meth_ty + (meth_scoped_tvs, meth_tvbs, meth_arg_kis, meth_res_ki) <- promote_meth_ty -- If ScopedTypeVariables is enabled, bring type variables into scope over the -- RHS. These type variables can come from the class/instance header, the -- method type signature/instance signature, or both, depending on how the @@ -647,9 +656,9 @@ promoteMethod meth_sort orig_sigs_map cls_tvb_names (meth_name, meth_rhs) = do -- we bring class/instance header type variables into scope but /not/ -- type variables from the class method/instance signature. scoped_tvs_ext <- qIsExtEnabled LangExt.ScopedTypeVariables - let meth_scoped_tvs + let all_meth_scoped_tvs | scoped_tvs_ext - = OSet.fromList (cls_tvb_names ++ map extractTvbName meth_tvbs) + = OSet.fromList (map extractTvbName cls_tvbs) `OSet.union` meth_scoped_tvs | otherwise = OSet.empty meth_arg_tvs <- replicateM (length meth_arg_kis) (qNewName "a") @@ -679,13 +688,34 @@ promoteMethod meth_sort orig_sigs_map cls_tvb_names (meth_name, meth_rhs) = do family_args = map DVarT meth_arg_tvs helperName <- newUniqueName helperNameBase let proHelperName = promotedValueName opts helperName Nothing + -- If a promoted method's kind lacks an outermost `forall`, then we need + -- to compute the list of kind variable binders manually. The order of + -- these binders doesn't matter, as the user will never invoke a helper + -- type family directly, so we simply quantify the binders in + -- left-to-right order. + full_meth_tvbs + | null meth_tvbs + = changeDTVFlags SpecifiedSpec $ + toposortTyVarsOf (meth_arg_kis ++ [meth_res_ki]) + | otherwise + = meth_tvbs + -- Make sure not to re-quantify any kind variable binders that are already + -- bound by the class or instance head. + full_meth_tvbs_without_cls_tvbs = + deleteFirstsBy ((==) `on` extractTvbName) full_meth_tvbs cls_tvbs + -- All of the kind variable binders, including both (1) those bound by the + -- class or instance head, and (2) those bound by the promoted method's + -- kind. This will be used in an outermost `forall` in the helper type + -- family's standalone kind signature to specify the kinds of kind + -- variables (when possible). + all_meth_tvbs = cls_tvbs ++ full_meth_tvbs_without_cls_tvbs -- Promote the right-hand side of the helper. Note that we never partially -- apply the helper type family, and users will never invoke the helper -- directly. As such, there is no need to emit defunctionalization symbols for -- the helper type family. (pro_decs, _defun_decs, ann_rhs) - <- promoteLetDecRHS (ClassMethodRHS meth_scoped_tvs meth_arg_kis meth_res_ki) + <- promoteLetDecRHS (ClassMethodRHS all_meth_scoped_tvs all_meth_tvbs meth_arg_kis meth_res_ki) OMap.empty OMap.empty Nothing helperName meth_rhs emitDecs pro_decs @@ -703,18 +733,42 @@ promoteMethod meth_sort orig_sigs_map cls_tvb_names (meth_name, meth_rhs) = do -- `instance C T`, then the substitution [a |-> T] must be applied to the -- original method's type.) -- - -- This returns three things in a tuple: + -- This returns four things in a tuple: + -- + -- 1. The set of scoped type variables from the class method signature or + -- instance signature. If an instance method lacks an instance signature, + -- this will be an empty set. These type variables will be brought into + -- scope over the RHS of the method: see Note [Scoped type variables and + -- class methods] in D.S.TH.Promote.Monad. + -- + -- 2. The list of kind variable binders that are explicitly quantified by an + -- outermost `forall` in the promoted type. If there is no such outermost + -- `forall`, then this will be the empty list. + -- + -- 3. The promoted argument kinds. + -- + -- 4. The promoted result kind. + -- + -- Note that: -- - -- * The list of scoped type variables from the class method signature or - -- instance signature. If an instance method lacks an instance signature, - -- this will be an empty list. These type variables will be brought into - -- scope over the RHS of the method: see Note [Scoped type variables and - -- class methods] in D.S.TH.Promote.Monad. + -- * Ultimately, this information is used to compute a standalone kind + -- signature for a "helper" type family which defines the promoted version + -- of a class method default or instance method. Because users never + -- invoke helper type families directly, it is not important to get the + -- order of kind variables exactly right. As such, the list of kind + -- variable binders can be in an unspecified order. -- - -- * The promoted argument kinds. + -- * The kind variable binders only include kind variables that are + -- quantified by the /method/, not by the class or instance head. The + -- variables bound by the class or instance head are added separately + -- (see `all_meth_tvbs` above). -- - -- * The promoted result kind. - promote_meth_ty :: PrM ([DTyVarBndrSpec], [DKind], DKind) + -- * The set of scoped type variable names will always be a subset of the + -- names in the list of kind variable binders. We are using the kind + -- variable binders primarily as a way to annotate the kinds of each + -- variable, so it is possible for the helper type family to bind a kind + -- variable in a `forall` without it scoping over the body. + promote_meth_ty :: PrM (OSet Name, [DTyVarBndrSpec], [DKind], DKind) promote_meth_ty = case meth_sort of DefaultMethods -> @@ -728,29 +782,33 @@ promoteMethod meth_sort orig_sigs_map cls_tvb_names (meth_name, meth_rhs) = do -- We have an InstanceSig. These are easy: we can just use the -- instance signature's type directly, and no substitution for -- class variables is required. - promoteUnraveled ty + (kvbs, arg_kis, res_ki) <- promoteUnraveled ty + pure (OSet.fromList (map extractTvbName kvbs), kvbs, arg_kis, res_ki) Nothing -> do -- We don't have an InstanceSig, so we must compute the kind to use -- ourselves. - (_, arg_kis, res_ki) <- lookup_meth_ty + (_, kvbs, arg_kis, res_ki) <- lookup_meth_ty -- Substitute for the class variables in the method's type. -- See Note [Promoted class method kinds] - let arg_kis' = map (substKind cls_subst) arg_kis + let kvbs' = mapDTVKind (substKind cls_subst) <$> kvbs + arg_kis' = map (substKind cls_subst) arg_kis res_ki' = substKind cls_subst res_ki -- If there is no instance signature, then there are no additional - -- type variables to bring into scope, so return an empty list of - -- scoped type variables. - pure ([], arg_kis', res_ki') + -- type variables to bring into scope, so return an empty set of + -- scoped type variables. We will reuse the list of kind variable + -- binders in case they have useful kind information. + pure (OSet.empty, kvbs', arg_kis', res_ki') -- Attempt to look up a class method's original type. - lookup_meth_ty :: PrM ([DTyVarBndrSpec], [DKind], DKind) + lookup_meth_ty :: PrM (OSet Name, [DTyVarBndrSpec], [DKind], DKind) lookup_meth_ty = do opts <- getOptions let proName = promotedTopLevelValueName opts meth_name case OMap.lookup meth_name orig_sigs_map of Just ty -> do -- The type of the method is in scope, so promote that. - promoteUnraveled ty + (kvbs, arg_kis, res_ki) <- promoteUnraveled ty + pure (OSet.fromList (map extractTvbName kvbs), kvbs, arg_kis, res_ki) Nothing -> do -- If the type of the method is not in scope, the only other option -- is to try reifying the promoted method name. @@ -762,8 +820,12 @@ promoteMethod meth_sort orig_sigs_map cls_tvb_names (meth_name, meth_rhs) = do res_ki = defaultMaybeToTypeKind (resultSigToMaybeKind mb_res_ki) -- If there is no instance signature, then there are no -- additional type variables to bring into scope, so return an - -- empty list of scoped type variables. - in pure ([], arg_kis, res_ki) + -- empty set of scoped type variables. Moreover, we do not + -- have a list of kind variable binders readily available, so + -- we return an empty list. This is OK, as we will compute + -- the kind variable binders for the helper type family + -- elsewhere (see `full_meth_tvbs` above). + in pure (OSet.empty, [], arg_kis, res_ki) _ -> fail $ "Cannot find type annotation for " ++ show proName {- @@ -929,6 +991,12 @@ data LetDecRHSSort -- the RHS of the class method. See -- Note [Scoped type variables and class methods] -- in D.S.TH.Promote.Monad. + [DTyVarBndrSpec] + -- The RHS's kind variable binders. Note that we do not + -- guarantee a particular order for these binders (see + -- Note [Promoted class methods and kind variable ordering]), + -- as we are mainly using kind variable binders for the sake + -- of annotating variables with their kinds. [DKind] -- The RHS's promoted argument kinds. Needed to fix #136. DKind -- The RHS's promoted result kind. Needed to fix #136. deriving Show @@ -1073,19 +1141,9 @@ promoteLetDecRHS rhs_sort type_env fix_env mb_let_uniq name let_dec_rhs = do -- will default to the earlier Int argument. promote_let_dec_ty all_locals default_num_args = case rhs_sort of - ClassMethodRHS scoped_tvs arg_kis res_ki - -> -- Class method RHS helper functions are only used internally, so - -- there's no point in trying to get the order of type variables - -- correct. Nevertheless, we /do/ want to bind the type variables - -- in an outermost `forall` so that we can bring any scoped type - -- variables into scope. As such, we simply quantify the type - -- variables from left to right. - -- See Note [Scoped type variables and class methods] in - -- D.S.TH.Promote.Monad. - let sak_tvbs = changeDTVFlags SpecifiedSpec $ - toposortTyVarsOf $ arg_kis ++ [res_ki] - sak = ravelVanillaDType sak_tvbs [] arg_kis res_ki in - return (Just (LDRKI (Just sak) scoped_tvs sak_tvbs arg_kis res_ki), length arg_kis) + ClassMethodRHS scoped_tvs tvbs arg_kis res_ki + -> let sak = ravelVanillaDType tvbs [] arg_kis res_ki in + return (Just (LDRKI (Just sak) scoped_tvs tvbs arg_kis res_ki), length arg_kis) LetBindingRHS | Just ty <- OMap.lookup name type_env -> do