diff options
Diffstat (limited to 'compiler/GHC/Tc/Utils')
| -rw-r--r-- | compiler/GHC/Tc/Utils/Env.hs | 4 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Instantiate.hs | 29 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Monad.hs | 4 | ||||
| -rw-r--r-- | compiler/GHC/Tc/Utils/Unify.hs | 15 |
4 files changed, 37 insertions, 15 deletions
diff --git a/compiler/GHC/Tc/Utils/Env.hs b/compiler/GHC/Tc/Utils/Env.hs index 7755d3370d..b989ade11a 100644 --- a/compiler/GHC/Tc/Utils/Env.hs +++ b/compiler/GHC/Tc/Utils/Env.hs @@ -733,8 +733,8 @@ tcAddDataFamConPlaceholders inst_decls thing_inside = concatMap (get_fi_cons . unLoc) fids get_fi_cons :: DataFamInstDecl GhcRn -> [Name] - get_fi_cons (DataFamInstDecl { dfid_eqn = HsIB { hsib_body = - FamEqn { feqn_rhs = HsDataDefn { dd_cons = cons } }}}) + get_fi_cons (DataFamInstDecl { dfid_eqn = + FamEqn { feqn_rhs = HsDataDefn { dd_cons = cons } }}) = map unLoc $ concatMap (getConNames . unLoc) cons diff --git a/compiler/GHC/Tc/Utils/Instantiate.hs b/compiler/GHC/Tc/Utils/Instantiate.hs index 5416e29692..debbbe1341 100644 --- a/compiler/GHC/Tc/Utils/Instantiate.hs +++ b/compiler/GHC/Tc/Utils/Instantiate.hs @@ -492,7 +492,7 @@ tcInstTypeBndrs id tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType) -- Instantiate a type signature with skolem constants. --- We could give them fresh names, but no need to do so +-- This freshens the names, but no need to do so tcSkolDFunType dfun = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun ; return (map snd tv_prs, theta, tau) } @@ -524,13 +524,18 @@ tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- See Note [Skolemising type variables] +-- This version freshens the names and creates "super skolems"; +-- see comments around superSkolemTv. tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- See Note [Skolemising type variables] +-- This version freshens the names and creates "super skolems"; +-- see comments around superSkolemTv. tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst -tcInstSkolTyVarsPushLevel :: Bool -> TCvSubst -> [TyVar] +tcInstSkolTyVarsPushLevel :: Bool -- True <=> make "super skolem" + -> TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar]) -- Skolemise one level deeper, hence pushTcLevel -- See Note [Skolemising type variables] @@ -599,10 +604,22 @@ a) Level allocation. We generally skolemise /before/ calling b) The [TyVar] should be ordered (kind vars first) See Note [Kind substitution when instantiating] -c) It's a complete freshening operation: the skolems have a fresh - unique, and a location from the monad - -d) The resulting skolems are +c) Clone the variable to give a fresh unique. This is essential. + Consider (tc160) + type Foo x = forall a. a -> x + And typecheck the expression + (e :: Foo (Foo ()) + We will skolemise the signature, but after expanding synonyms it + looks like + forall a. a -> forall a. a -> x + We don't want to make two big-lambdas with the same unique! + +d) We retain locations. Because the location of the variable is the correct + location to report in errors (e.g. in the signature). We don't want the + location to change to the body of the function, which does *not* explicitly + bind the variable. + +e) The resulting skolems are non-overlappable for tcInstSkolTyVars, but overlappable for tcInstSuperSkolTyVars See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs index e42fe42799..0ff826bb96 100644 --- a/compiler/GHC/Tc/Utils/Monad.hs +++ b/compiler/GHC/Tc/Utils/Monad.hs @@ -1845,8 +1845,8 @@ It's distressingly delicate though: the visible type application fails in the monad (throws an exception). We must not discard the out-of-scope error. - Also GHC.Tc.Solver.emitFlatConstraints may fail having emitted some - constraints with skolem-escape problems. + Also GHC.Tc.Solver.simplifyAndEmitFlatConstraints may fail having + emitted some constraints with skolem-escape problems. * If we discard too /few/ constraints, we may get the misleading class constraints mentioned above. But we may /also/ end up taking diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs index c1202f02d7..b8e946ac11 100644 --- a/compiler/GHC/Tc/Utils/Unify.hs +++ b/compiler/GHC/Tc/Utils/Unify.hs @@ -927,13 +927,18 @@ checkTvConstraints skol_info skol_tvs thing_inside emitResidualTvConstraint :: SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM () emitResidualTvConstraint skol_info skol_tvs tclvl wanted - | isEmptyWC wanted - = return () - - | otherwise - = do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted + | not (isEmptyWC wanted) || + checkTelescopeSkol skol_info + = -- checkTelescopeSkol: in this case, /always/ emit this implication + -- even if 'wanted' is empty. We need the implication so that we check + -- for a bad telescope. See Note [Skolem escape and forall-types] in + -- GHC.Tc.Gen.HsType + do { implic <- buildTvImplication skol_info skol_tvs tclvl wanted ; emitImplication implic } + | otherwise -- Empty 'wanted', emit nothing + = return () + buildTvImplication :: SkolemInfo -> [TcTyVar] -> TcLevel -> WantedConstraints -> TcM Implication buildTvImplication skol_info skol_tvs tclvl wanted |