[Git][ghc/ghc][wip/int-index/retry-instds] Draft: retry instance declarations
Vladislav Zavialov (@int-index)
gitlab at gitlab.haskell.org
Sun Feb 23 12:57:30 UTC 2025
Vladislav Zavialov pushed to branch wip/int-index/retry-instds at Glasgow Haskell Compiler / GHC
Commits:
410f03ba by Vladislav Zavialov at 2025-02-23T15:56:19+03:00
Draft: retry instance declarations
Metric Increase:
T1969
- - - - -
15 changed files:
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/Tc/TyCl/Instance.hs
- compiler/GHC/Tc/TyCl/Instance.hs-boot
- + testsuite/tests/dependent/should_compile/T12088a.hs
- + testsuite/tests/dependent/should_compile/T12088b.hs
- + testsuite/tests/dependent/should_compile/T12088c.hs
- + testsuite/tests/dependent/should_compile/T12088sg1.hs
- + testsuite/tests/dependent/should_compile/T12088sg2.hs
- + testsuite/tests/dependent/should_compile/T12239.hs
- + testsuite/tests/dependent/should_compile/T14668a.hs
- + testsuite/tests/dependent/should_compile/T14668b.hs
- + testsuite/tests/dependent/should_compile/T22257a.hs
- + testsuite/tests/dependent/should_compile/T22257b.hs
- + testsuite/tests/dependent/should_compile/T25238.hs
- testsuite/tests/dependent/should_compile/all.T
Changes:
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -45,7 +45,7 @@ import GHC.Tc.Zonk.Type
import GHC.Tc.Zonk.TcType
import GHC.Tc.TyCl.Utils
import GHC.Tc.TyCl.Class
-import {-# SOURCE #-} GHC.Tc.TyCl.Instance( tcInstDecls1 )
+import {-# SOURCE #-} GHC.Tc.TyCl.Instance( tryTcInstDecls1, tcInstDecls1 )
import {-# SOURCE #-} GHC.Tc.Module( checkBootDeclM )
import GHC.Tc.Deriv (DerivInfo(..))
import GHC.Tc.Gen.HsType
@@ -161,28 +161,45 @@ tcTyAndClassDecls tyclds_s
-- The code recovers internally, but if anything gave rise to
-- an error we'd better stop now, to avoid a cascade
-- Type check each group in dependency order folding the global env
- = checkNoErrs $ fold_env [] [] emptyNameEnv tyclds_s
+ = checkNoErrs $ fold_env [] [] [] emptyNameEnv tyclds_s
where
- fold_env :: [InstInfo GhcRn]
+ fold_env :: [LInstDecl GhcRn]
+ -> [InstInfo GhcRn]
-> [DerivInfo]
-> ThBindEnv
-> [TyClGroup GhcRn]
-> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ThBindEnv)
- fold_env inst_info deriv_info th_bndrs []
- = do { gbl_env <- getGblEnv
- ; return (gbl_env, inst_info, deriv_info, th_bndrs) }
- fold_env inst_info deriv_info th_bndrs (tyclds:tyclds_s)
- = do { (tcg_env, inst_info', deriv_info', th_bndrs')
- <- tcTyClGroup tyclds
+ fold_env pending_instds inst_info deriv_info th_bndrs []
+ = do { (gbl_env, inst_info', deriv_info', th_bndrs') <- tcInstDecls1 pending_instds
+ ; return (gbl_env,
+ inst_info' ++ inst_info,
+ deriv_info' ++ deriv_info,
+ th_bndrs' `plusNameEnv` th_bndrs) }
+ fold_env pending_instds inst_info deriv_info th_bndrs (tyclds:tyclds_s)
+ = do { (failed_instds, tcg_env, inst_info', deriv_info', th_bndrs') <- tcTyClGroup tyclds
+ ; let retry_pending = length failed_instds < length (group_instds tyclds)
+ -- if progress on instances has been made, we can retry the pending ones
+ (pending_instds', tyclds_s')
+ | retry_pending = ([], mkInstDeclGroup (pending_instds ++ failed_instds) : tyclds_s)
+ | otherwise = (pending_instds ++ failed_instds, tyclds_s)
; setGblEnv tcg_env $
-- remaining groups are typechecked in the extended global env.
- fold_env (inst_info' ++ inst_info)
+ fold_env pending_instds'
+ (inst_info' ++ inst_info)
(deriv_info' ++ deriv_info)
(th_bndrs' `plusNameEnv` th_bndrs)
- tyclds_s }
+ tyclds_s' }
+
+mkInstDeclGroup :: [LInstDecl GhcRn] -> TyClGroup GhcRn
+mkInstDeclGroup instds =
+ TyClGroup { group_ext = noExtField
+ , group_tyclds = []
+ , group_roles = []
+ , group_kisigs = []
+ , group_instds = instds }
tcTyClGroup :: TyClGroup GhcRn
- -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ThBindEnv)
+ -> TcM ([LInstDecl GhcRn], TcGblEnv, [InstInfo GhcRn], [DerivInfo], ThBindEnv)
-- Typecheck one strongly-connected component of type, class, and instance decls
-- See Note [TyClGroups and dependency analysis] in GHC.Hs.Decls
tcTyClGroup (TyClGroup { group_tyclds = tyclds
@@ -238,14 +255,14 @@ tcTyClGroup (TyClGroup { group_tyclds = tyclds
; (gbl_env, th_bndrs) <- addTyConsToGblEnv tyclss
-- Step 4: check instance declarations
- ; (gbl_env', inst_info, datafam_deriv_info, th_bndrs') <-
+ ; (failed_instds, gbl_env', inst_info, datafam_deriv_info, th_bndrs') <-
setGblEnv gbl_env $
- tcInstDecls1 instds
+ tryTcInstDecls1 instds
; let deriv_info = datafam_deriv_info ++ data_deriv_info
; let gbl_env'' = gbl_env'
{ tcg_ksigs = tcg_ksigs gbl_env' `unionNameSet` kindless }
- ; return (gbl_env'', inst_info, deriv_info,
+ ; return (failed_instds, gbl_env'', inst_info, deriv_info,
th_bndrs' `plusNameEnv` th_bndrs) }
-- Gives the kind for every TyCon that has a standalone kind signature
=====================================
compiler/GHC/Tc/TyCl/Instance.hs
=====================================
@@ -14,7 +14,8 @@
-- | Typechecking instance declarations
module GHC.Tc.TyCl.Instance
- ( tcInstDecls1
+ ( tryTcInstDecls1
+ , tcInstDecls1
, tcInstDeclsDeriv
, tcInstDecls2
)
@@ -91,7 +92,7 @@ import qualified GHC.LanguageExtensions as LangExt
import Control.Monad
import Data.Tuple
import GHC.Data.Maybe
-import Data.List( mapAccumL )
+import Data.List( mapAccumL, unzip4 )
{-
@@ -386,6 +387,39 @@ complained if 'b' is mentioned in <rhs>.
Gather up the instance declarations from their various sources
-}
+tryTcInstDecls1 -- Deal with both source-code and imported instance decls
+ :: [LInstDecl GhcRn] -- Source code instance decls
+ -> TcM ([LInstDecl GhcRn], -- Failed instances
+ TcGblEnv, -- The full inst env
+ [InstInfo GhcRn], -- Source-code instance decls to process;
+ -- contains all dfuns for this module
+ [DerivInfo], -- From data family instances
+ ThBindEnv) -- TH binding levels
+
+tryTcInstDecls1 inst_decls
+ = do { -- Do class and family instance declarations
+
+ ; traceTc "tryTcInstDecls1 {" (text "n=" <> ppr (length inst_decls))
+ ; stuff <- mapM tryTcLocalInstDecl inst_decls
+
+ ; let (failed_inst_decls_s, local_infos_s, fam_insts_s, datafam_deriv_infos_s) = unzip4 stuff
+ failed_inst_decls = concat failed_inst_decls_s
+ fam_insts = concat fam_insts_s
+ local_infos = concat local_infos_s
+ datafam_deriv_infos = concat datafam_deriv_infos_s
+
+ ; (gbl_env, th_bndrs) <-
+ addClsInsts local_infos $
+ addFamInsts fam_insts
+
+ ; traceTc "} tryTcInstDecls1 " (text "failed:" <+> ppr failed_inst_decls)
+
+ ; return ( failed_inst_decls
+ , gbl_env
+ , local_infos
+ , datafam_deriv_infos
+ , th_bndrs ) }
+
tcInstDecls1 -- Deal with both source-code and imported instance decls
:: [LInstDecl GhcRn] -- Source code instance decls
-> TcM (TcGblEnv, -- The full inst env
@@ -396,11 +430,13 @@ tcInstDecls1 -- Deal with both source-code and imported instance decls
tcInstDecls1 inst_decls
= do { -- Do class and family instance declarations
+
; stuff <- mapAndRecoverM tcLocalInstDecl inst_decls
- ; let (local_infos_s, fam_insts_s, datafam_deriv_infos) = unzip3 stuff
- fam_insts = concat fam_insts_s
- local_infos = concat local_infos_s
+ ; let (local_infos_s, fam_insts_s, datafam_deriv_infos_s) = unzip3 stuff
+ fam_insts = concat fam_insts_s
+ local_infos = concat local_infos_s
+ datafam_deriv_infos = concat datafam_deriv_infos_s
; (gbl_env, th_bndrs) <-
addClsInsts local_infos $
@@ -408,7 +444,7 @@ tcInstDecls1 inst_decls
; return ( gbl_env
, local_infos
- , concat datafam_deriv_infos
+ , datafam_deriv_infos
, th_bndrs ) }
-- | Use DerivInfo for data family instances (produced by tcInstDecls1),
@@ -483,6 +519,14 @@ tcLocalInstDecl (L loc (ClsInstD { cid_inst = decl }))
= do { (insts, fam_insts, deriv_infos) <- tcClsInstDecl (L loc decl)
; return (insts, fam_insts, deriv_infos) }
+tryTcLocalInstDecl :: LInstDecl GhcRn
+ -> TcM ([LInstDecl GhcRn], [InstInfo GhcRn], [FamInst], [DerivInfo])
+tryTcLocalInstDecl inst =
+ tryTcDiscardingErrs recover (success <$> tcLocalInstDecl inst)
+ where
+ recover = return ([inst], [], [], [])
+ success (insts, fam_insts, deriv_infos) = ([], insts, fam_insts, deriv_infos)
+
tcClsInstDecl :: LClsInstDecl GhcRn
-> TcM ([InstInfo GhcRn], [FamInst], [DerivInfo])
-- The returned DerivInfos are for any associated data families
=====================================
compiler/GHC/Tc/TyCl/Instance.hs-boot
=====================================
@@ -3,7 +3,7 @@
(c) The GRASP/AQUA Project, Glasgow University, 1992-1998
-}
-module GHC.Tc.TyCl.Instance ( tcInstDecls1 ) where
+module GHC.Tc.TyCl.Instance ( tryTcInstDecls1, tcInstDecls1 ) where
import GHC.Hs
import GHC.Tc.Types
@@ -12,5 +12,8 @@ import GHC.Tc.Deriv
-- We need this because of the mutual recursion
-- between GHC.Tc.TyCl and GHC.Tc.TyCl.Instance
+tryTcInstDecls1 :: [LInstDecl GhcRn]
+ -> TcM ([LInstDecl GhcRn], TcGblEnv, [InstInfo GhcRn], [DerivInfo], ThBindEnv)
+
tcInstDecls1 :: [LInstDecl GhcRn]
- -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ThBindEnv)
+ -> TcM (TcGblEnv, [InstInfo GhcRn], [DerivInfo], ThBindEnv)
\ No newline at end of file
=====================================
testsuite/tests/dependent/should_compile/T12088a.hs
=====================================
@@ -0,0 +1,17 @@
+{-# LANGUAGE DataKinds, TypeFamilies, UndecidableInstances #-}
+
+module T12088a where
+
+import Data.Kind
+import GHC.TypeLits
+
+type family Open a
+type instance Open Bool = Nat
+type instance Open Float = Type
+type instance Open Char = F Float
+
+type F :: forall a -> Open a
+type family F a
+type instance F Bool = 42
+type instance F Float = [Nat]
+type instance F Char = '[0, 1]
=====================================
testsuite/tests/dependent/should_compile/T12088b.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE DataKinds, TypeFamilies #-}
+
+module T12088b where
+
+import Data.Kind
+
+type family IxKind (m :: Type) :: Type
+type family Value (m :: Type) :: IxKind m -> Type
+data T (k :: Type) (f :: k -> Type) = MkT
+
+type instance IxKind (T k f) = k
+type instance Value (T k f) = f
\ No newline at end of file
=====================================
testsuite/tests/dependent/should_compile/T12088c.hs
=====================================
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds, TypeFamilies #-}
+
+module T12088c where
+
+import Data.Kind
+
+type family K a
+
+class C a where -- C:def
+ type F a :: K a -- F:sig
+ type G a :: K a -- G:sig
+
+data T
+
+type instance K T = Type
+
+instance C T where -- C:inst
+ type F T = Bool -- F:def
+ type G T = String -- G:def
\ No newline at end of file
=====================================
testsuite/tests/dependent/should_compile/T12088sg1.hs
=====================================
@@ -0,0 +1,30 @@
+{-# LANGUAGE TypeFamilies, DataKinds, TemplateHaskell #-}
+
+-- Based on singleton-gadts
+module T12088sg1 where
+
+import Data.Kind (Type)
+
+type Promote :: Type -> Type
+type family Promote k
+
+type PromoteX :: k -> Promote k
+type family PromoteX a
+
+type Demote :: Type -> Type
+type family Demote k
+
+type DemoteX :: k -> Demote k
+type family DemoteX a
+
+$(return [])
+
+type instance Demote [a] = [Demote a]
+type instance Promote [a] = [Promote a]
+
+type instance DemoteX '[] = '[]
+type instance DemoteX (x:xs) = DemoteX x : DemoteX xs
+
+type instance PromoteX '[] = '[]
+type instance PromoteX (x:xs) = PromoteX x : PromoteX xs
+
=====================================
testsuite/tests/dependent/should_compile/T12088sg2.hs
=====================================
@@ -0,0 +1,22 @@
+{-# LANGUAGE TypeFamilies, DataKinds, TemplateHaskell #-}
+
+-- Based on singletons-gadts
+module T12088sg2 where
+
+import Data.Kind
+
+type family Demote (k :: Type) :: Type
+type family DemoteX (a :: k) :: Demote k
+
+type instance Demote Type = Type
+type instance DemoteX (a :: Type) = Demote a
+
+data TyFun :: Type -> Type -> Type
+
+$(return [])
+
+data TyCon1 :: (k1 -> k2) -> TyFun k1 k2 -> Type
+
+type instance Demote (TyFun a b -> Type) = DemoteX a -> DemoteX b
+type instance DemoteX (TyCon1 (Either a)) = Either (DemoteX a)
+
=====================================
testsuite/tests/dependent/should_compile/T12239.hs
=====================================
@@ -0,0 +1,23 @@
+{-# LANGUAGE PolyKinds, DataKinds, GADTs, TypeFamilies #-}
+
+module T12239 where
+
+import Data.Kind (Type)
+
+data N = Z | S N
+
+data Fin :: N -> Type where
+ FZ :: Fin (S n)
+ FS :: Fin n -> Fin (S n)
+
+type family FieldCount (t :: Type) :: N
+
+type family FieldType (t :: Type) (i :: Fin (FieldCount t)) :: Type
+
+data T
+
+type instance FieldCount T = S (S (S Z))
+
+type instance FieldType T FZ = Int
+type instance FieldType T (FS FZ) = Bool
+type instance FieldType T (FS (FS FZ)) = String
=====================================
testsuite/tests/dependent/should_compile/T14668a.hs
=====================================
@@ -0,0 +1,21 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T14668a where
+
+data G (b :: ()) = G
+
+class C a where
+ type family F a
+
+class (C a) => C' a where
+ type family F' a (b :: F a)
+
+data CInst
+
+instance C CInst where
+ type F CInst = ()
+
+instance C' CInst where
+ type F' CInst (b :: F CInst) = G b
+
=====================================
testsuite/tests/dependent/should_compile/T14668b.hs
=====================================
@@ -0,0 +1,21 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE DataKinds #-}
+
+module T14668b where
+
+import Prelude
+import Data.Kind
+
+type family KeyKind (obj :: Type) :: Type
+type family ValKind (obj :: Type) :: Type
+
+type family Get (key :: KeyKind a) (obj :: a) :: ValKind a
+
+data Map (k :: Type) (v :: Type) = Map [(k,v)]
+
+type instance KeyKind (Map k v) = k
+type instance ValKind (Map k v) = v
+
+type instance Get k ('Map ('(k,v) ': _)) = v
+
=====================================
testsuite/tests/dependent/should_compile/T22257a.hs
=====================================
@@ -0,0 +1,14 @@
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module T22257a where
+
+import Data.Kind (Type)
+
+type family F (x :: Type) :: Type
+type family G (x :: Type) (y :: F x) :: Type
+
+$(return [])
+
+type instance F () = Type
+type instance G () k = k
=====================================
testsuite/tests/dependent/should_compile/T22257b.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module T22257b where
+
+import Data.Kind (Type)
+
+type family F (x :: Type) :: Type
+type family G (x :: Type) (y :: F x) :: Type
+
+data T
+type instance F T = Type
+type instance G T k = k
=====================================
testsuite/tests/dependent/should_compile/T25238.hs
=====================================
@@ -0,0 +1,22 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE PolyKinds #-}
+
+module T25238 where
+
+import Data.Kind
+
+data MsgDef = MsgDoThis
+
+type family Msg c
+type instance Msg X = MsgDef
+
+type family FromPat c :: Msg c
+
+data X
+
+type Id a = a
+
+type instance FromPat X = MsgDoThis
+type instance FromPat X = (MsgDoThis :: Msg X)
+type instance FromPat X = (MsgDoThis :: Id (Msg X))
=====================================
testsuite/tests/dependent/should_compile/all.T
=====================================
@@ -64,3 +64,14 @@ test('T18660', normal, compile, [''])
test('T12174', normal, compile, [''])
test('LopezJuan', normal, compile, [''])
test('T25387', normal, compile, [''])
+test('T12239', normal, compile, [''])
+test('T12088a', normal, compile, [''])
+test('T12088b', normal, compile, [''])
+test('T12088c', normal, compile, [''])
+test('T12088sg1', normal, compile, [''])
+test('T12088sg2', normal, compile, [''])
+test('T14668a', normal, compile, [''])
+test('T14668b', normal, compile, [''])
+test('T22257a', normal, compile, [''])
+test('T22257b', normal, compile, [''])
+test('T25238', normal, compile, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/410f03ba4a66c101da50581818c324580dbabc39
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/410f03ba4a66c101da50581818c324580dbabc39
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20250223/df679538/attachment-0001.html>
More information about the ghc-commits
mailing list