Commit f59aad68 authored by Edward Z. Yang's avatar Edward Z. Yang

Fix handling of closed type families in Backpack.

Summary:
A few related problems:

- CoAxioms, like DFuns, are implicit and never exported,
  so we have to make sure we treat them the same way as
  DFuns: in RnModIface we need to rename references to
  them with rnIfaceImplicit and in mergeSignatures we need
  to NOT check them directly for compatibility (the
  test on the type family will do this check for us.)

- But actually, we weren't checking if the axioms WERE
  consistent.  This is because we were forwarding all
  embedded CoAxiom references in the type family TyThing
  to the merged version, but that reference was what
  checkBootDeclM was using as a comparison point.
  This is similar to a problem we saw with DFuns.

  To fix this, I refactored the handling of implicit entities in TcIface
  for Backpack.  See Note [The implicit TypeEnv] for the gory details.
  Instead of passing the TypeEnv around explicitly, we stuffed it in
  IfLclEnv.
Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>

Test Plan: validate

Reviewers: bgamari, simonpj, austin

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2928
parent 8744869e
......@@ -466,7 +466,7 @@ rnIfaceDecl d@IfaceClass{} = do
, ifSigs = sigs
}
rnIfaceDecl d@IfaceAxiom{} = do
name <- rnIfaceGlobal (ifName d)
name <- rnIfaceImplicit (ifName d)
tycon <- rnIfaceTyCon (ifTyCon d)
ax_branches <- mapM rnIfaceAxBranch (ifAxBranches d)
return d { ifName = name
......@@ -497,7 +497,7 @@ rnIfaceDecl d@IfacePatSyn{} = do
rnIfaceFamTyConFlav :: Rename IfaceFamTyConFlav
rnIfaceFamTyConFlav (IfaceClosedSynFamilyTyCon (Just (n, axs)))
= IfaceClosedSynFamilyTyCon . Just <$> ((,) <$> rnIfaceGlobal n
= IfaceClosedSynFamilyTyCon . Just <$> ((,) <$> rnIfaceImplicit n
<*> mapM rnIfaceAxBranch axs)
rnIfaceFamTyConFlav flav = pure flav
......
......@@ -7,6 +7,7 @@ Type checking of type signatures in interface files
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE NondecreasingIndentation #-}
module TcIface (
tcLookupImported_maybe,
......@@ -204,6 +205,7 @@ typecheckIface iface
isAbstractIfaceDecl :: IfaceDecl -> Bool
isAbstractIfaceDecl IfaceData{ ifCons = IfAbstractTyCon _ } = True
isAbstractIfaceDecl IfaceClass{ ifCtxt = [], ifSigs = [], ifATs = [] } = True
isAbstractIfaceDecl IfaceFamily{ ifFamFlav = IfaceAbstractClosedSynFamilyTyCon } = True
isAbstractIfaceDecl _ = False
-- | Merge two 'IfaceDecl's together, preferring a non-abstract one. If
......@@ -276,7 +278,7 @@ typecheckIfacesForMerging mod ifaces tc_env_var =
ignore_prags <- goptM Opt_IgnoreInterfacePragmas
-- Build the initial environment
-- NB: Don't include dfuns here, because we don't want to
-- serialize them out. See Note [Bogus DFun renamings]
-- serialize them out. See Note [Bogus DFun renamings] in RnModIface
let mk_decl_env decls
= mkOccEnv [ (getOccName decl, decl)
| decl <- decls
......@@ -295,13 +297,15 @@ typecheckIfacesForMerging mod ifaces tc_env_var =
-- OK, now typecheck each ModIface using this environment
details <- forM ifaces $ \iface -> do
-- DO NOT load these decls into the mutable variable: we did
-- that already!
decls <- loadDecls ignore_prags (mi_decls iface)
let type_env = mkNameEnv decls
-- See Note [The implicit TypeEnv]
type_env <- fixM $ \type_env -> do
setImplicitEnvM type_env $ do
decls <- loadDecls ignore_prags (mi_decls iface)
return (mkNameEnv decls)
-- But note that we use this type_env to typecheck references to DFun
-- in 'IfaceInst'
insts <- mapM (tcIfaceInstWithDFunTypeEnv type_env) (mi_insts iface)
setImplicitEnvM type_env $ do
insts <- mapM tcIfaceInst (mi_insts iface)
fam_insts <- mapM tcIfaceFamInst (mi_fam_insts iface)
rules <- tcIfaceRules ignore_prags (mi_rules iface)
anns <- tcIfaceAnnotations (mi_anns iface)
......@@ -333,10 +337,14 @@ typecheckIfaceForInstantiate nsubst iface =
(text "typecheckIfaceForInstantiate")
(mi_boot iface) nsubst $ do
ignore_prags <- goptM Opt_IgnoreInterfacePragmas
decls <- loadDecls ignore_prags (mi_decls iface)
let type_env = mkNameEnv decls
-- See Note [The implicit TypeEnv]
type_env <- fixM $ \type_env -> do
setImplicitEnvM type_env $ do
decls <- loadDecls ignore_prags (mi_decls iface)
return (mkNameEnv decls)
-- See Note [Bogus DFun renamings]
insts <- mapM (tcIfaceInstWithDFunTypeEnv type_env) (mi_insts iface)
setImplicitEnvM type_env $ do
insts <- mapM tcIfaceInst (mi_insts iface)
fam_insts <- mapM tcIfaceFamInst (mi_fam_insts iface)
rules <- tcIfaceRules ignore_prags (mi_rules iface)
anns <- tcIfaceAnnotations (mi_anns iface)
......@@ -351,6 +359,33 @@ typecheckIfaceForInstantiate nsubst iface =
, md_exports = exports
}
-- Note [The implicit TypeEnv]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- As described in 'typecheckIfacesForMerging', the splendid innovation
-- of signature merging is to rewrite all Names in each of the signatures
-- we are merging together to a pre-merged structure; this is the key
-- ingredient that lets us solve some problems when merging type
-- synonyms.
--
-- However in the case of DFuns and CoAxioms, this strategy goes
-- *too far*. In particular, the reference to a DFun or CoAxiom in
-- an instance declaration or closed type family (respectively) will
-- refer to the merged declaration. However, checkBootDeclM only
-- ever looks at the embedded structure when performing its comparison;
-- by virtue of the fact that everything's been pointed to the merged
-- declaration, you'll never notice there's a difference even if there
-- is one.
--
-- The solution is, for reference to implicit entities, we go straight
-- for the local TypeEnv corresponding to the entities from this particular
-- signature; this logic is in 'tcIfaceImplicit'.
--
-- There is also some fixM business because families need to refer to
-- coercion axioms, which are all in the big pile of decls. I didn't
-- feel like untangling first so the fixM is a convenient way to get things
-- where they need to be.
--
{-
************************************************************************
* *
......@@ -858,25 +893,7 @@ tcIfaceInst (IfaceClsInst { ifDFun = dfun_name, ifOFlag = oflag
, ifInstCls = cls, ifInstTys = mb_tcs
, ifInstOrph = orph })
= do { dfun <- forkM (text "Dict fun" <+> ppr dfun_name) $
tcIfaceExtId dfun_name
; let mb_tcs' = map (fmap ifaceTyConName) mb_tcs
; return (mkImportedInstance cls mb_tcs' dfun_name dfun oflag orph) }
-- | Typecheck an 'IfaceClsInst', but rather than using 'tcIfaceGlobal',
-- resolve the 'ifDFun' using a passed in 'TypeEnv'.
--
-- Why do we do it this way? See Note [Bogus DFun renamings]
tcIfaceInstWithDFunTypeEnv :: TypeEnv -> IfaceClsInst -> IfL ClsInst
tcIfaceInstWithDFunTypeEnv tenv
(IfaceClsInst { ifDFun = dfun_name, ifOFlag = oflag
, ifInstCls = cls, ifInstTys = mb_tcs
, ifInstOrph = orph })
= do { dfun <- case lookupTypeEnv tenv dfun_name of
Nothing -> pprPanic "tcIfaceInstWithDFunTypeEnv"
(ppr dfun_name $$ ppr tenv)
Just (AnId dfun) -> return dfun
Just tything -> pprPanic "tcIfaceInstWithDFunTypeEnv"
(ppr dfun_name <+> ppr tything)
fmap tyThingId (tcIfaceImplicit dfun_name)
; let mb_tcs' = map (fmap ifaceTyConName) mb_tcs
; return (mkImportedInstance cls mb_tcs' dfun_name dfun oflag orph) }
......@@ -1618,7 +1635,7 @@ tcIfaceTyCon (IfaceTyCon name info)
IsPromoted -> promoteDataCon $ tyThingDataCon thing }
tcIfaceCoAxiom :: Name -> IfL (CoAxiom Branched)
tcIfaceCoAxiom name = do { thing <- tcIfaceGlobal name
tcIfaceCoAxiom name = do { thing <- tcIfaceImplicit name
; return (tyThingCoAxiom thing) }
tcIfaceDataCon :: Name -> IfL DataCon
......@@ -1633,6 +1650,17 @@ tcIfaceExtId name = do { thing <- tcIfaceGlobal name
AnId id -> return id
_ -> pprPanic "tcIfaceExtId" (ppr name$$ ppr thing) }
-- See Note [The implicit TypeEnv]
tcIfaceImplicit :: Name -> IfL TyThing
tcIfaceImplicit n = do
lcl_env <- getLclEnv
case if_implicits_env lcl_env of
Nothing -> tcIfaceGlobal n
Just tenv ->
case lookupTypeEnv tenv n of
Nothing -> pprPanic "tcIfaceInst" (ppr n $$ ppr tenv)
Just tything -> return tything
{-
************************************************************************
* *
......
......@@ -135,6 +135,8 @@ checkHsigIface tcg_env gr sig_iface
dfun_names = map getName sig_insts
check_export name
-- Skip instances, we'll check them later
-- TODO: Actually this should never happen, because DFuns are
-- never exported...
| name `elem` dfun_names = return ()
-- See if we can find the type directly in the hsig ModDetails
-- TODO: need to special case wired in names
......@@ -559,23 +561,23 @@ mergeSignatures hsmod lcl_iface0 = do
tcg_env <- (\x -> foldM x tcg_env infos)
$ \tcg_env (iface, details) -> do
-- For every TyThing in the type environment, compare it for
-- compatibility with the merged environment, but skip
-- DFunIds and implicit TyThings.
let check_ty sig_thing
-- We'll check these with the parent
| isImplicitTyThing sig_thing
= return ()
-- These aren't in the type environment; checked
-- when merging instances
| AnId id <- sig_thing
, isDFunId id
= return ()
| Just thing <- lookupTypeEnv type_env (getName sig_thing)
= checkHsigDeclM iface sig_thing thing
let check_export name
| Just sig_thing <- lookupTypeEnv (md_types details) name
= case lookupTypeEnv type_env (getName sig_thing) of
Just thing -> checkHsigDeclM iface sig_thing thing
Nothing -> panic "mergeSignatures: check_export"
-- Oops! We're looking for this export but it's
-- not actually in the type environment of the signature's
-- ModDetails.
--
-- NB: This case happens because the we're iterating
-- over the union of all exports, so some interfaces
-- won't have everything. Note that md_exports is nonsense
-- (it's the same as exports); maybe we should fix this
-- eventually.
| otherwise
= panic "mergeSignatures check_ty"
mapM_ check_ty (typeEnvElts (md_types details))
= return ()
mapM_ check_export (map availName exports)
-- Note [Signature merging instances]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -1066,6 +1066,8 @@ checkBootTyCon is_boot tc1 tc2
= ASSERT(tc1 == tc2)
let eqFamFlav OpenSynFamilyTyCon OpenSynFamilyTyCon = True
eqFamFlav (DataFamilyTyCon {}) (DataFamilyTyCon {}) = True
-- This case only happens for hsig merging:
eqFamFlav AbstractClosedSynFamilyTyCon AbstractClosedSynFamilyTyCon = True
eqFamFlav AbstractClosedSynFamilyTyCon (ClosedSynFamilyTyCon {}) = True
eqFamFlav (ClosedSynFamilyTyCon {}) AbstractClosedSynFamilyTyCon = True
eqFamFlav (ClosedSynFamilyTyCon ax1) (ClosedSynFamilyTyCon ax2)
......@@ -1077,8 +1079,11 @@ checkBootTyCon is_boot tc1 tc2
in
-- check equality of roles, family flavours and injectivity annotations
check (roles1 == roles2) roles_msg `andThenCheck`
check (eqFamFlav fam_flav1 fam_flav2) empty `andThenCheck`
check (injInfo1 == injInfo2) empty
check (eqFamFlav fam_flav1 fam_flav2)
(ifPprDebug $
text "Family flavours" <+> ppr fam_flav1 <+> text "and" <+> ppr fam_flav2 <+>
text "do not match") `andThenCheck`
check (injInfo1 == injInfo2) (text "Injectivities do not match")
| isAlgTyCon tc1 && isAlgTyCon tc2
, Just env <- eqVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
......
......@@ -124,6 +124,7 @@ module TcRnMonad(
failIfM,
forkM_maybe,
forkM,
setImplicitEnvM,
withException,
......@@ -1670,6 +1671,7 @@ mkIfLclEnv mod loc boot
if_loc = loc,
if_boot = boot,
if_nsubst = Nothing,
if_implicits_env = Nothing,
if_tv_env = emptyFsEnv,
if_id_env = emptyFsEnv }
......@@ -1800,6 +1802,9 @@ forkM doc thing_inside
-- pprPanic "forkM" doc
Just r -> r) }
setImplicitEnvM :: TypeEnv -> IfL a -> IfL a
setImplicitEnvM tenv m = updLclEnv (\lcl -> lcl { if_implicits_env = Just tenv }) m
{-
Note [Masking exceptions in forkM_maybe]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -321,6 +321,13 @@ data IfLclEnv
if_nsubst :: Maybe NameShape,
-- This field is used to make sure "implicit" declarations
-- (anything that cannot be exported in mi_exports) get
-- wired up correctly in typecheckIfacesForMerging. Most
-- of the time it's @Nothing@. See Note [The implicit TypeEnv]
-- in TcIface.
if_implicits_env :: Maybe TypeEnv,
if_tv_env :: FastStringEnv TyVar, -- Nested tyvar bindings
if_id_env :: FastStringEnv Id -- Nested id binding
}
......
......@@ -997,6 +997,14 @@ data FamTyConFlav
-- | Built-in type family used by the TypeNats solver
| BuiltInSynFamTyCon BuiltInSynFamily
instance Outputable FamTyConFlav where
ppr (DataFamilyTyCon n) = text "data family" <+> ppr n
ppr OpenSynFamilyTyCon = text "open type family"
ppr (ClosedSynFamilyTyCon Nothing) = text "closed type family"
ppr (ClosedSynFamilyTyCon (Just coax)) = text "closed type family" <+> ppr coax
ppr AbstractClosedSynFamilyTyCon = text "abstract closed type family"
ppr (BuiltInSynFamTyCon _) = text "built-in type family"
{- Note [Closed type families]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* In an open type family you can add new instances later. This is the
......
......@@ -39,3 +39,5 @@ test('bkp44', normal, backpack_compile, [''])
test('bkp45', normal, backpack_compile, [''])
test('bkp46', normal, backpack_compile, [''])
test('bkp47', normal, backpack_compile, [''])
test('bkp48', normal, backpack_compile, [''])
test('bkp49', normal, backpack_compile, [''])
{-# LANGUAGE TypeFamilies #-}
unit p where
signature A where
type family K a where ..
unit q where
signature A where
type family K a where
K a = Int
unit r where
dependency p[A=<A>]
dependency q[A=<A>]
unit i where
module A where
type family K a where
K a = Int
unit m where
dependency r[A=i:A]
dependency p[A=i:A]
dependency q[A=i:A]
[1 of 5] Processing p
[1 of 1] Compiling A[sig] ( p/A.hsig, nothing )
[2 of 5] Processing q
[1 of 1] Compiling A[sig] ( q/A.hsig, nothing )
[3 of 5] Processing r
[1 of 1] Compiling A[sig] ( r/A.hsig, nothing )
[4 of 5] Processing i
Instantiating i
[1 of 1] Compiling A ( i/A.hs, bkp48.out/i/A.o )
[5 of 5] Processing m
Instantiating m
[1 of 3] Including r[A=i:A]
Instantiating r[A=i:A]
[1 of 2] Including p[A=i:A]
Instantiating p[A=i:A]
[1 of 1] Compiling A[sig] ( p/A.hsig, bkp48.out/p/p-CtJxD03mJqIIVJzOga8l4X/A.o )
[2 of 2] Including q[A=i:A]
Instantiating q[A=i:A]
[1 of 1] Compiling A[sig] ( q/A.hsig, bkp48.out/q/q-CtJxD03mJqIIVJzOga8l4X/A.o )
[1 of 1] Compiling A[sig] ( r/A.hsig, bkp48.out/r/r-CtJxD03mJqIIVJzOga8l4X/A.o )
[2 of 3] Including p[A=i:A]
[3 of 3] Including q[A=i:A]
unit p where
signature A where
data T
instance Eq T
unit q where
dependency p[A=<A>]
signature A (T) where
[1 of 2] Processing p
[1 of 1] Compiling A[sig] ( p/A.hsig, nothing )
[2 of 2] Processing q
[1 of 1] Compiling A[sig] ( q/A.hsig, nothing )
......@@ -37,3 +37,4 @@ test('bkpfail38', normal, backpack_compile_fail, [''])
test('bkpfail39', expect_broken(13068), backpack_compile_fail, [''])
test('bkpfail40', normal, backpack_compile_fail, [''])
test('bkpfail41', normal, backpack_compile_fail, [''])
test('bkpfail42', normal, backpack_compile_fail, [''])
{-# LANGUAGE TypeFamilies #-}
unit p where
signature A where
type family F a where
F a = Bool
unit q where
dependency p[A=<A>]
signature A where
type family F a where
F a = Int
[1 of 2] Processing p
[1 of 1] Compiling A[sig] ( p/A.hsig, nothing )
[2 of 2] Processing q
[1 of 1] Compiling A[sig] ( q/A.hsig, nothing )
bkpfail42.bkp:9:9: error:
Type constructor ‘F’ has conflicting definitions in the module
and its hsig file
Main module: type family F a :: *
where [a] F a = GHC.Types.Int
Hsig file: type family F a :: *
where [a] F a = GHC.Types.Bool
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment