diff options
| -rw-r--r-- | compiler/hsSyn/HsUtils.lhs | 15 | ||||
| -rw-r--r-- | compiler/typecheck/FamInst.lhs | 78 | ||||
| -rw-r--r-- | compiler/typecheck/TcDeriv.lhs | 28 | ||||
| -rw-r--r-- | compiler/typecheck/TcErrors.lhs | 49 | ||||
| -rw-r--r-- | compiler/typecheck/TcEvidence.lhs | 21 | ||||
| -rw-r--r-- | compiler/typecheck/TcExpr.lhs | 46 | ||||
| -rw-r--r-- | compiler/typecheck/TcInteract.lhs | 88 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.lhs | 19 | ||||
| -rw-r--r-- | compiler/types/Coercion.lhs | 6 | ||||
| -rw-r--r-- | compiler/types/FamInstEnv.lhs | 31 | ||||
| -rw-r--r-- | compiler/types/TyCon.lhs | 9 | ||||
| -rw-r--r-- | compiler/types/Type.lhs | 22 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T9580.hs | 7 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T9580.stderr | 10 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/T9580a.hs | 5 | ||||
| -rw-r--r-- | testsuite/tests/indexed-types/should_fail/all.T | 1 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr | 3 |
17 files changed, 220 insertions, 218 deletions
diff --git a/compiler/hsSyn/HsUtils.lhs b/compiler/hsSyn/HsUtils.lhs index 4b5bdb4d66..35de6a6bde 100644 --- a/compiler/hsSyn/HsUtils.lhs +++ b/compiler/hsSyn/HsUtils.lhs @@ -29,7 +29,7 @@ module HsUtils( mkHsPar, mkHsApp, mkHsConApp, mkSimpleHsAlt, mkSimpleMatch, unguardedGRHSs, unguardedRHS, mkMatchGroup, mkMatchGroupName, mkMatch, mkHsLam, mkHsIf, - mkHsWrap, mkLHsWrap, mkHsWrapCo, mkLHsWrapCo, + mkHsWrap, mkLHsWrap, mkHsWrapCo, mkHsWrapCoR, mkLHsWrapCo, coToHsWrapper, mkHsDictLet, mkHsLams, mkHsOpApp, mkHsDo, mkHsComp, mkHsWrapPat, mkHsWrapPatCo, mkLHsPar, mkHsCmdCast, @@ -487,9 +487,14 @@ mkHsWrap :: HsWrapper -> HsExpr id -> HsExpr id mkHsWrap co_fn e | isIdHsWrapper co_fn = e | otherwise = HsWrap co_fn e -mkHsWrapCo :: TcCoercion -> HsExpr id -> HsExpr id +mkHsWrapCo :: TcCoercion -- A Nominal coercion a ~N b + -> HsExpr id -> HsExpr id mkHsWrapCo co e = mkHsWrap (coToHsWrapper co) e +mkHsWrapCoR :: TcCoercion -- A Representational coercion a ~R b + -> HsExpr id -> HsExpr id +mkHsWrapCoR co e = mkHsWrap (coToHsWrapperR co) e + mkLHsWrapCo :: TcCoercion -> LHsExpr id -> LHsExpr id mkLHsWrapCo co (L loc e) = L loc (mkHsWrapCo co e) @@ -497,10 +502,14 @@ mkHsCmdCast :: TcCoercion -> HsCmd id -> HsCmd id mkHsCmdCast co cmd | isTcReflCo co = cmd | otherwise = HsCmdCast co cmd -coToHsWrapper :: TcCoercion -> HsWrapper +coToHsWrapper :: TcCoercion -> HsWrapper -- A Nominal coercion coToHsWrapper co | isTcReflCo co = idHsWrapper | otherwise = mkWpCast (mkTcSubCo co) +coToHsWrapperR :: TcCoercion -> HsWrapper -- A Representational coercion +coToHsWrapperR co | isTcReflCo co = idHsWrapper + | otherwise = mkWpCast co + mkHsWrapPat :: HsWrapper -> Pat id -> Type -> Pat id mkHsWrapPat co_fn p ty | isIdHsWrapper co_fn = p | otherwise = CoPat co_fn p ty diff --git a/compiler/typecheck/FamInst.lhs b/compiler/typecheck/FamInst.lhs index d0b2d0da5a..b917491af2 100644 --- a/compiler/typecheck/FamInst.lhs +++ b/compiler/typecheck/FamInst.lhs @@ -9,10 +9,11 @@ The @FamInst@ type: family instance heads -- http://ghc.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#TabsvsSpaces -- for details -module FamInst ( +module FamInst ( + FamInstEnvs, tcGetFamInstEnvs, checkFamInstConsistency, tcExtendLocalFamInstEnv, - tcLookupFamInst, - tcGetFamInstEnvs, + tcLookupFamInst, + tcLookupDataFamInst, tcInstNewTyConTF_maybe, tcInstNewTyCon_maybe, newFamInst ) where @@ -20,7 +21,9 @@ import HscTypes import FamInstEnv import InstEnv( roughMatchTcs ) import Coercion( pprCoAxBranchHdr ) +import TcEvidence import LoadIface +import Type( applyTysX ) import TypeRep import TcRnMonad import TyCon @@ -35,7 +38,6 @@ import Maybes import TcMType import TcType import Name -import VarSet import Control.Monad import Data.Map (Map) import qualified Data.Map as Map @@ -210,24 +212,60 @@ then we have a coercion (ie, type instance of family instance coercion) which implies that :R42T was declared as 'data instance T [a]'. \begin{code} -tcLookupFamInst :: TyCon -> [Type] -> TcM (Maybe FamInstMatch) -tcLookupFamInst tycon tys +tcLookupFamInst :: FamInstEnvs -> TyCon -> [Type] -> Maybe FamInstMatch +tcLookupFamInst fam_envs tycon tys | not (isOpenFamilyTyCon tycon) - = return Nothing + = Nothing | otherwise - = do { instEnv <- tcGetFamInstEnvs - ; let mb_match = lookupFamInstEnv instEnv tycon tys - ; traceTc "lookupFamInst" $ - vcat [ ppr tycon <+> ppr tys - , pprTvBndrs (varSetElems (tyVarsOfTypes tys)) - , ppr mb_match - -- , ppr instEnv - ] - ; case mb_match of - [] -> return Nothing - (match:_) - -> return $ Just match - } + = case lookupFamInstEnv fam_envs tycon tys of + match : _ -> Just match + [] -> Nothing + +-- | If @co :: T ts ~ rep_ty@ then: +-- +-- > instNewTyCon_maybe T ts = Just (rep_ty, co) +-- +-- Checks for a newtype, and for being saturated +-- Just like Coercion.instNewTyCon_maybe, but returns a TcCoercion +tcInstNewTyCon_maybe :: TyCon -> [TcType] -> Maybe (TcType, TcCoercion) +tcInstNewTyCon_maybe tc tys + | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype + , tvs `leLength` tys -- Check saturated enough + = Just (applyTysX tvs ty tys, mkTcUnbranchedAxInstCo Representational co_tc tys) + | otherwise + = Nothing + +tcLookupDataFamInst :: FamInstEnvs -> TyCon -> [TcType] + -> (TyCon, [TcType], TcCoercion) +-- ^ Converts a data family type (eg F [a]) to its representation type (eg FList a) +-- and returns a coercion between the two: co :: F [a] ~R FList a +-- If there is no instance, or it's not a data family, just return +-- Refl coercion and the original inputs +tcLookupDataFamInst fam_inst_envs tc tc_args + | isDataFamilyTyCon tc + , match : _ <- lookupFamInstEnv fam_inst_envs tc tc_args + , FamInstMatch { fim_instance = rep_fam + , fim_tys = rep_args } <- match + , let co_tc = famInstAxiom rep_fam + rep_tc = dataFamInstRepTyCon rep_fam + co = mkTcUnbranchedAxInstCo Representational co_tc rep_args + = (rep_tc, rep_args, co) + + | otherwise + = (tc, tc_args, mkTcNomReflCo (mkTyConApp tc tc_args)) + +tcInstNewTyConTF_maybe :: FamInstEnvs -> TcType -> Maybe (TyCon, TcType, TcCoercion) +-- ^ If (instNewTyConTF_maybe envs ty) returns Just (ty', co) +-- then co :: ty ~R ty' +-- ty is (D tys) is a newtype (possibly after looking through the type family D) +-- ty' is the RHS type of the of (D tys) newtype +tcInstNewTyConTF_maybe fam_envs ty + | Just (tc, tc_args) <- tcSplitTyConApp_maybe ty + , let (rep_tc, rep_tc_args, fam_co) = tcLookupDataFamInst fam_envs tc tc_args + , Just (inner_ty, nt_co) <- tcInstNewTyCon_maybe rep_tc rep_tc_args + = Just (rep_tc, inner_ty, fam_co `mkTcTransCo` nt_co) + | otherwise + = Nothing \end{code} diff --git a/compiler/typecheck/TcDeriv.lhs b/compiler/typecheck/TcDeriv.lhs index a14d29eee5..af05e80a08 100644 --- a/compiler/typecheck/TcDeriv.lhs +++ b/compiler/typecheck/TcDeriv.lhs @@ -888,9 +888,14 @@ mkEqnHelp overlap_mode tvs cls cls_tys tycon tc_args mtheta IsValid -> mkOldTypeableEqn tvs cls tycon tc_args mtheta } | otherwise - = do { (rep_tc, rep_tc_args) <- lookup_data_fam tycon tc_args - -- Be careful to test rep_tc here: in the case of families, - -- we want to check the instance tycon, not the family tycon + = do { -- Find the instance of a data family + -- Note [Looking up family instances for deriving] + fam_envs <- tcGetFamInstEnvs + ; let (rep_tc, rep_tc_args, _co) = tcLookupDataFamInst fam_envs tycon tc_args + + -- If it's still a data family, the lookup failed; i.e no instance exists + ; when (isDataFamilyTyCon rep_tc) + (bale_out (ptext (sLit "No family instance for") <+> quotes (pprTypeApp tycon tc_args))) -- For standalone deriving (mtheta /= Nothing), -- check that all the data constructors are in scope. @@ -923,23 +928,6 @@ mkEqnHelp overlap_mode tvs cls cls_tys tycon tc_args mtheta tycon tc_args rep_tc rep_tc_args mtheta } where bale_out msg = failWithTc (derivingThingErr False cls cls_tys (mkTyConApp tycon tc_args) msg) - - lookup_data_fam :: TyCon -> [Type] -> TcM (TyCon, [Type]) - -- Find the instance of a data family - -- Note [Looking up family instances for deriving] - lookup_data_fam tycon tys - | not (isFamilyTyCon tycon) - = return (tycon, tys) - | otherwise - = ASSERT( isAlgTyCon tycon ) - do { maybeFamInst <- tcLookupFamInst tycon tys - ; case maybeFamInst of - Nothing -> bale_out (ptext (sLit "No family instance for") - <+> quotes (pprTypeApp tycon tys)) - Just (FamInstMatch { fim_instance = famInst - , fim_tys = tys }) - -> let tycon' = dataFamInstRepTyCon famInst - in return (tycon', tys) } \end{code} Note [Looking up family instances for deriving] diff --git a/compiler/typecheck/TcErrors.lhs b/compiler/typecheck/TcErrors.lhs index c8f3d06997..57f9829432 100644 --- a/compiler/typecheck/TcErrors.lhs +++ b/compiler/typecheck/TcErrors.lhs @@ -25,6 +25,7 @@ import Type import Kind ( isKind ) import Unify ( tcMatchTys ) import Module +import FamInst ( FamInstEnvs, tcGetFamInstEnvs, tcLookupDataFamInst ) import Inst import InstEnv import TyCon @@ -983,18 +984,19 @@ Warn of loopy local equalities that were dropped. \begin{code} mkDictErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg -mkDictErr ctxt cts +mkDictErr ctxt cts = ASSERT( not (null cts) ) do { inst_envs <- tcGetInstEnvs + ; fam_envs <- tcGetFamInstEnvs ; lookups <- mapM (lookup_cls_inst inst_envs) cts ; let (no_inst_cts, overlap_cts) = partition is_no_inst lookups - -- Report definite no-instance errors, + -- Report definite no-instance errors, -- or (iff there are none) overlap errors -- But we report only one of them (hence 'head') because they all -- have the same source-location origin, to try avoid a cascade -- of error from one location - ; (ctxt, err) <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts)) + ; (ctxt, err) <- mk_dict_err fam_envs ctxt (head (no_inst_cts ++ overlap_cts)) ; mkErrorMsg ctxt ct1 err } where ct1:_ = elim_superclasses cts @@ -1022,11 +1024,11 @@ mkDictErr ctxt cts where min_preds = mkMinimalBySCs (map ctPred cts) -mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult) +mk_dict_err :: FamInstEnvs -> ReportErrCtxt -> (Ct, ClsInstLookupResult) -> TcM (ReportErrCtxt, SDoc) -- Report an overlap error if this class constraint results -- from an overlap (returning Left clas), otherwise return (Right pred) -mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell)) +mk_dict_err fam_envs ctxt (ct, (matches, unifiers, safe_haskell)) | null matches -- No matches but perhaps several unifiers = do { let (is_ambig, ambig_msg) = mkAmbigMsg ct ; (ctxt, binds_msg) <- relevantBindings True ctxt ct @@ -1190,11 +1192,13 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell)) | (n,Nominal,t1,t2) <- zip4 [1..] (tyConRoles tc1) tyArgs1 tyArgs2 , not (t1 `eqType` t2) ] - | Just (tc,_) <- splitTyConApp_maybe ty1, - Just msg <- coercible_msg_for_tycon rdr_env tc + | Just (tc, tys) <- tcSplitTyConApp_maybe ty1 + , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys + , Just msg <- coercible_msg_for_tycon rdr_env rep_tc = msg - | Just (tc,_) <- splitTyConApp_maybe ty2, - Just msg <- coercible_msg_for_tycon rdr_env tc + | Just (tc, tys) <- splitTyConApp_maybe ty2 + , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys + , Just msg <- coercible_msg_for_tycon rdr_env rep_tc = msg | otherwise = nest 2 $ sep [ ptext (sLit "because") <+> quotes (ppr ty1) @@ -1203,26 +1207,17 @@ mk_dict_err ctxt (ct, (matches, unifiers, safe_haskell)) where (ty1, ty2) = getEqPredTys pred - dataConMissing rdr_env tc = - all (null . lookupGRE_Name rdr_env) (map dataConName (tyConDataCons tc)) - coercible_msg_for_tycon rdr_env tc + | isAbstractTyCon tc + = Just $ hsep [ ptext $ sLit "because the type constructor", quotes (pprSourceTyCon tc) + , ptext $ sLit "is abstract" ] | isNewTyCon tc - = tyConAbstractMsg rdr_env tc empty - | otherwise - = Nothing - - tyConAbstractMsg rdr_env tc occExpl - | isAbstractTyCon tc || dataConMissing rdr_env tc = Just $ vcat $ - [ fsep [ ptext $ sLit "because the type constructor", quotes (ppr tc) <+> occExpl - , ptext $ sLit "is abstract" ] - | isAbstractTyCon tc - ] ++ - [ fsep [ ptext (sLit "because the constructor") <> plural (tyConDataCons tc) - , ptext (sLit "of") <+> quotes (ppr tc) <+> occExpl - , isOrAre (tyConDataCons tc) <+> ptext (sLit "not imported") ] - | dataConMissing rdr_env tc - ] + , [data_con] <- tyConDataCons tc + , let dc_name = dataConName data_con + , null (lookupGRE_Name rdr_env dc_name) + = Just $ hang (ptext (sLit "because the data constructor") <+> quotes (ppr dc_name)) + 2 (sep [ ptext (sLit "of newtype") <+> quotes (pprSourceTyCon tc) + , ptext (sLit "is not in scope") ]) | otherwise = Nothing show_fixes :: [SDoc] -> SDoc diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs index e2c2e60b04..8b64d2408b 100644 --- a/compiler/typecheck/TcEvidence.lhs +++ b/compiler/typecheck/TcEvidence.lhs @@ -28,14 +28,12 @@ module TcEvidence ( mkTcAxiomRuleCo, tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, isTcReflCo, getTcCoVar_maybe, - tcCoercionRole, eqVarRole, - coercionToTcCoercion + tcCoercionRole, eqVarRole ) where #include "HsVersions.h" import Var import Coercion( LeftOrRight(..), pickLR, nthRole ) -import qualified Coercion as C import PprCore () -- Instance OutputableBndr TyVar import TypeRep -- Knows type representation import TcType @@ -95,8 +93,6 @@ differences * TcAxiomInstCo has a [TcCoercion] parameter, and not a [Type] parameter. This differs from the formalism, but corresponds to AxiomInstCo (see [Coercion axioms applied to coercions]). - Why can't we use [TcType] here, in code not relevant for the simplifier? - Because of coercionToTcCoercion. \begin{code} data TcCoercion @@ -425,21 +421,6 @@ ppr_forall_co p ty split1 tvs ty = (reverse tvs, ty) \end{code} -Conversion from Coercion to TcCoercion -(at the moment, this is only needed to convert the result of -instNewTyConTF_maybe, so all unused cases are panics for now). - -\begin{code} -coercionToTcCoercion :: C.Coercion -> TcCoercion -coercionToTcCoercion = go - where - go (C.Refl r t) = TcRefl r t - go (C.TransCo c1 c2) = TcTransCo (go c1) (go c2) - go (C.AxiomInstCo coa ind cos) = TcAxiomInstCo coa ind (map go cos) - go (C.SubCo c) = TcSubCo (go c) - go (C.AppCo c1 c2) = TcAppCo (go c1) (go c2) - go co = pprPanic "coercionToTcCoercion" (ppr co) -\end{code} %************************************************************************ diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs index 6188842b72..29020b4cb9 100644 --- a/compiler/typecheck/TcExpr.lhs +++ b/compiler/typecheck/TcExpr.lhs @@ -26,8 +26,7 @@ import TcUnify import BasicTypes import Inst import TcBinds -import FamInst ( tcLookupFamInst ) -import FamInstEnv ( famInstAxiom, dataFamInstRepTyCon, FamInstMatch(..) ) +import FamInst ( tcGetFamInstEnvs, tcLookupDataFamInst ) import TcEnv import TcArrows import TcMatches @@ -1225,49 +1224,32 @@ tcTagToEnum loc fun_name arg res_ty ; let mb_tc_app = tcSplitTyConApp_maybe ty' Just (tc, tc_args) = mb_tc_app ; checkTc (isJust mb_tc_app) - (tagToEnumError ty' doc1) + (mk_error ty' doc1) -- Look through any type family - ; (coi, rep_tc, rep_args) <- get_rep_ty ty' tc tc_args + ; fam_envs <- tcGetFamInstEnvs + ; let (rep_tc, rep_args, coi) = tcLookupDataFamInst fam_envs tc tc_args + -- coi :: tc tc_args ~ rep_tc rep_args ; checkTc (isEnumerationTyCon rep_tc) - (tagToEnumError ty' doc2) + (mk_error ty' doc2) ; arg' <- tcMonoExpr arg intPrimTy ; let fun' = L loc (HsWrap (WpTyApp rep_ty) (HsVar fun)) rep_ty = mkTyConApp rep_tc rep_args - ; return (mkHsWrapCo coi $ HsApp fun' arg') } + ; return (mkHsWrapCoR (mkTcSymCo coi) $ HsApp fun' arg') } + -- coi is a Representational coercion where doc1 = vcat [ ptext (sLit "Specify the type by giving a type signature") , ptext (sLit "e.g. (tagToEnum# x) :: Bool") ] doc2 = ptext (sLit "Result type must be an enumeration type") - doc3 = ptext (sLit "No family instance for this type") - - get_rep_ty :: TcType -> TyCon -> [TcType] - -> TcM (TcCoercion, TyCon, [TcType]) - -- Converts a family type (eg F [a]) to its rep type (eg FList a) - -- and returns a coercion between the two - get_rep_ty ty tc tc_args - | not (isFamilyTyCon tc) - = return (mkTcNomReflCo ty, tc, tc_args) - | otherwise - = do { mb_fam <- tcLookupFamInst tc tc_args - ; case mb_fam of - Nothing -> failWithTc (tagToEnumError ty doc3) - Just (FamInstMatch { fim_instance = rep_fam - , fim_tys = rep_args }) - -> return ( mkTcSymCo (mkTcUnbranchedAxInstCo Nominal co_tc rep_args) - , rep_tc, rep_args ) - where - co_tc = famInstAxiom rep_fam - rep_tc = dataFamInstRepTyCon rep_fam } - -tagToEnumError :: TcType -> SDoc -> SDoc -tagToEnumError ty what - = hang (ptext (sLit "Bad call to tagToEnum#") - <+> ptext (sLit "at type") <+> ppr ty) - 2 what + + mk_error :: TcType -> SDoc -> SDoc + mk_error ty what + = hang (ptext (sLit "Bad call to tagToEnum#") + <+> ptext (sLit "at type") <+> ppr ty) + 2 what \end{code} diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs index 33249f4b04..e56c96131f 100644 --- a/compiler/typecheck/TcInteract.lhs +++ b/compiler/typecheck/TcInteract.lhs @@ -28,7 +28,7 @@ import Name import RdrName ( GlobalRdrEnv, lookupGRE_Name, mkRdrQual, is_as, is_decl, Provenance(Imported), gre_prov ) import FunDeps -import FamInstEnv ( FamInstEnvs, instNewTyConTF_maybe ) +import FamInst import TcEvidence import Outputable @@ -1820,29 +1820,27 @@ matchClassInst _ clas [ ty ] _ String -> SSymbol n SSymbol n -> KnownSymbol n -} - makeDict evLit = - case unwrapNewTyCon_maybe (classTyCon clas) of - Just (_,_, axDict) - | [ meth ] <- classMethods clas - , Just tcRep <- tyConAppTyCon_maybe -- SNat + makeDict evLit + | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty] + , [ meth ] <- classMethods clas + , Just tcRep <- tyConAppTyCon_maybe -- SNat $ funResultTy -- SNat n $ dropForAlls -- KnownNat n => SNat n $ idType meth -- forall n. KnownNat n => SNat n - , Just (_,_,axRep) <- unwrapNewTyCon_maybe tcRep - -> return $ - let co1 = mkTcSymCo $ mkTcUnbranchedAxInstCo Representational axRep [ty] - co2 = mkTcSymCo $ mkTcUnbranchedAxInstCo Representational axDict [ty] - in GenInst [] $ mkEvCast (EvLit evLit) (mkTcTransCo co1 co2) + , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty] + = return (GenInst [] $ mkEvCast (EvLit evLit) (mkTcTransCo co_dict co_rep)) - _ -> panicTcS (text "Unexpected evidence for" <+> ppr (className clas) + | otherwise + = panicTcS (text "Unexpected evidence for" <+> ppr (className clas) $$ vcat (map (ppr . idType) (classMethods clas))) matchClassInst _ clas [ _k, ty1, ty2 ] loc - | clas == coercibleClass = do - traceTcS "matchClassInst for" $ quotes (pprClassPred clas [ty1,ty2]) <+> text "at depth" <+> ppr (ctLocDepth loc) - ev <- getCoercibleInst loc ty1 ty2 - traceTcS "matchClassInst returned" $ ppr ev - return ev + | clas == coercibleClass + = do { traceTcS "matchClassInst for" $ + quotes (pprClassPred clas [ty1,ty2]) <+> text "at depth" <+> ppr (ctLocDepth loc) + ; ev <- getCoercibleInst loc ty1 ty2 + ; traceTcS "matchClassInst returned" $ ppr ev + ; return ev } matchClassInst inerts clas tys loc = do { dflags <- getDynFlags @@ -1927,11 +1925,11 @@ matchClassInst inerts clas tys loc -- See Note [Coercible Instances] -- Changes to this logic should likely be reflected in coercible_msg in TcErrors. getCoercibleInst :: CtLoc -> TcType -> TcType -> TcS LookupInstResult -getCoercibleInst loc ty1 ty2 = do - -- Get some global stuff in scope, for nice pattern-guard based code in `go` - rdr_env <- getGlobalRdrEnvTcS - famenv <- getFamInstEnvs - go famenv rdr_env +getCoercibleInst loc ty1 ty2 + = do { -- Get some global stuff in scope, for nice pattern-guard based code in `go` + rdr_env <- getGlobalRdrEnvTcS + ; famenv <- getFamInstEnvs + ; go famenv rdr_env } where go :: FamInstEnvs -> GlobalRdrEnv -> TcS LookupInstResult go famenv rdr_env @@ -1939,8 +1937,8 @@ getCoercibleInst loc ty1 ty2 = do -- Coercible a a (see case 1 in [Coercible Instances]) | ty1 `tcEqType` ty2 - = do return $ GenInst [] - $ EvCoercion (TcRefl Representational ty1) + = return $ GenInst [] + $ EvCoercion (TcRefl Representational ty1) -- Coercible (forall a. ty) (forall a. ty') (see case 2 in [Coercible Instances]) | tcIsForAllTy ty1 @@ -1948,33 +1946,29 @@ getCoercibleInst loc ty1 ty2 = do , let (tvs1,body1) = tcSplitForAllTys ty1 (tvs2,body2) = tcSplitForAllTys ty2 , equalLength tvs1 tvs2 - = do - ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2) - return $ GenInst [] ev_term + = do { ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2) + ; return $ GenInst [] ev_term } -- Coercible NT a (see case 3 in [Coercible Instances]) - | Just (tc,tyArgs) <- splitTyConApp_maybe ty1, - Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs, - dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon - = do markDataConsAsUsed rdr_env tc - ct_ev <- requestCoercible loc concTy ty2 - local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred concTy ty2 - let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev))) - tcCo = TcLetCo binds $ - coercionToTcCoercion ntCo `mkTcTransCo` mkTcCoVarCo local_var - return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo) + | Just (rep_tc, concTy, ntCo) <- tcInstNewTyConTF_maybe famenv ty1 + , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon + = do { markDataConsAsUsed rdr_env rep_tc + ; ct_ev <- requestCoercible loc concTy ty2 + ; local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred concTy ty2 + ; let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev))) + tcCo = TcLetCo binds (ntCo `mkTcTransCo` mkTcCoVarCo local_var) + ; return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo) } -- Coercible a NT (see case 3 in [Coercible Instances]) - | Just (tc,tyArgs) <- splitTyConApp_maybe ty2, - Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs, - dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon - = do markDataConsAsUsed rdr_env tc - ct_ev <- requestCoercible loc ty1 concTy - local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred ty1 concTy - let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev))) - tcCo = TcLetCo binds $ - mkTcCoVarCo local_var `mkTcTransCo` mkTcSymCo (coercionToTcCoercion ntCo) - return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo) + | Just (rep_tc, concTy, ntCo) <- tcInstNewTyConTF_maybe famenv ty2 + , dataConsInScope rdr_env rep_tc -- Do not look at all tyConsOfTyCon + = do { markDataConsAsUsed rdr_env rep_tc + ; ct_ev <- requestCoercible loc ty1 concTy + ; local_var <- mkSysLocalM (fsLit "coev") $ mkCoerciblePred ty1 concTy + ; let binds = EvBinds (unitBag (EvBind local_var (getEvTerm ct_ev))) + tcCo = TcLetCo binds $ + mkTcCoVarCo local_var `mkTcTransCo` mkTcSymCo ntCo + ; return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo) } -- Coercible (D ty1 ty2) (D ty1' ty2') (see case 4 in [Coercible Instances]) | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1, diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index 9891f77795..4cb679d49b 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -86,7 +86,7 @@ module TcSMonad ( getDefaultInfo, getDynFlags, getGlobalRdrEnvTcS, - matchFam, matchOpenFam, + matchFam, checkWellStagedDFun, pprEq -- Smaller utils, re-exported from TcM -- TODO (DV): these are only really used in the @@ -122,6 +122,7 @@ import Name import RdrName (RdrName, GlobalRdrEnv) import RnEnv (addUsedRdrNames) import Var +import VarSet import VarEnv import Outputable import Bag @@ -145,7 +146,6 @@ import Data.IORef import Data.List( partition ) #ifdef DEBUG -import VarSet import Digraph #endif \end{code} @@ -1863,20 +1863,21 @@ rewriteEqEvidence old_ev swapped nlhs nrhs lhs_co rhs_co where new_pred = mkTcEqPred nlhs nrhs -maybeSym :: SwapFlag -> TcCoercion -> TcCoercion +maybeSym :: SwapFlag -> TcCoercion -> TcCoercion maybeSym IsSwapped co = mkTcSymCo co maybeSym NotSwapped co = co - -matchOpenFam :: TyCon -> [Type] -> TcS (Maybe FamInstMatch) -matchOpenFam tycon args = wrapTcS $ tcLookupFamInst tycon args - matchFam :: TyCon -> [Type] -> TcS (Maybe (TcCoercion, TcType)) -- Given (F tys) return (ty, co), where co :: F tys ~ ty matchFam tycon args | isOpenSynFamilyTyCon tycon - = do { maybe_match <- matchOpenFam tycon args - ; case maybe_match of + = do { fam_envs <- getFamInstEnvs + ; let mb_match = tcLookupFamInst fam_envs tycon args + ; traceTcS "lookupFamInst" $ + vcat [ ppr tycon <+> ppr args + , pprTvBndrs (varSetElems (tyVarsOfTypes args)) + , ppr mb_match ] + ; case mb_match of Nothing -> return Nothing Just (FamInstMatch { fim_instance = famInst , fim_tys = inst_tys }) diff --git a/compiler/types/Coercion.lhs b/compiler/types/Coercion.lhs index f0c0516c0e..fc6c8a7669 100644 --- a/compiler/types/Coercion.lhs +++ b/compiler/types/Coercion.lhs @@ -1228,9 +1228,9 @@ mkCoCast c g -- Checks for a newtype, and for being saturated instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion) instNewTyCon_maybe tc tys - | Just (tvs, ty, co_tc) <- unwrapNewTyCon_maybe tc -- Check for newtype - , tys `lengthIs` tyConArity tc -- Check saturated - = Just (substTyWith tvs tys ty, mkUnbranchedAxInstCo Representational co_tc tys) + | Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc -- Check for newtype + , tvs `leLength` tys -- Check saturated enough + = Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys) | otherwise = Nothing diff --git a/compiler/types/FamInstEnv.lhs b/compiler/types/FamInstEnv.lhs index 1308984f4f..3ff9e3be7c 100644 --- a/compiler/types/FamInstEnv.lhs +++ b/compiler/types/FamInstEnv.lhs @@ -23,11 +23,10 @@ module FamInstEnv ( FamInstMatch(..), lookupFamInstEnv, lookupFamInstEnvConflicts, - - isDominatedBy, + chooseBranch, isDominatedBy, -- Normalisation - instNewTyConTF_maybe, chooseBranch, topNormaliseType, topNormaliseType_maybe, + topNormaliseType, topNormaliseType_maybe, normaliseType, normaliseTcApp, -- Flattening @@ -863,7 +862,6 @@ findBranch (CoAxBranch { cab_tvs = tpl_tvs, cab_lhs = tpl_lhs, cab_incomps = inc -- fail if no branches left findBranch [] _ _ = Nothing - \end{code} @@ -874,29 +872,6 @@ findBranch [] _ _ = Nothing %************************************************************************ \begin{code} --- | Unwrap a newtype of a newtype intances. This is analogous to --- Coercion.instNewTyCon_maybe; differences are: --- * it also lookups up newtypes families, and --- * it does not require the newtype to be saturated. --- (a requirement using it for Coercible) -instNewTyConTF_maybe :: FamInstEnvs -> TyCon -> [Type] -> Maybe (Type, Coercion) -instNewTyConTF_maybe env tc tys = result - where - (co1, tc2, tys2) - | Just (co, rhs1) <- reduceTyFamApp_maybe env Representational tc tys - , Just (tc2, tys2) <- splitTyConApp_maybe rhs1 - = (co, tc2, tys2) - | otherwise - = (mkReflCo Representational (mkTyConApp tc tys), tc, tys) - - result - | Just (_, _, co_tc) <- unwrapNewTyCon_maybe tc2 -- Check for newtype - , newTyConEtadArity tc2 <= length tys2 -- Check for enough arguments - = Just (newTyConInstRhs tc2 tys2 - , co1 `mkTransCo` mkUnbranchedAxInstCo Representational co_tc tys2) - | otherwise - = Nothing - topNormaliseType :: FamInstEnvs -> Type -> Type topNormaliseType env ty = case topNormaliseType_maybe env ty of Just (_co, ty') -> ty' @@ -963,7 +938,7 @@ normaliseTcApp env role tc tys -- we do not do anything = let (co, ntys) = normaliseTcArgs env role tc tys in (co, mkTyConApp tc ntys) - + --------------- normaliseTcArgs :: FamInstEnvs -- environment with family instances diff --git a/compiler/types/TyCon.lhs b/compiler/types/TyCon.lhs index 65b5645d74..64a2a6cc3c 100644 --- a/compiler/types/TyCon.lhs +++ b/compiler/types/TyCon.lhs @@ -73,7 +73,8 @@ module TyCon( synTyConDefn_maybe, synTyConRhs_maybe, tyConExtName, -- External name for foreign types algTyConRhs, - newTyConRhs, newTyConEtadArity, newTyConEtadRhs, unwrapNewTyCon_maybe, + newTyConRhs, newTyConEtadArity, newTyConEtadRhs, + unwrapNewTyCon_maybe, unwrapNewTyConEtad_maybe, tupleTyConBoxity, tupleTyConSort, tupleTyConArity, -- ** Manipulating TyCons @@ -1170,6 +1171,12 @@ unwrapNewTyCon_maybe (AlgTyCon { tyConTyVars = tvs, = Just (tvs, rhs, co) unwrapNewTyCon_maybe _ = Nothing +unwrapNewTyConEtad_maybe :: TyCon -> Maybe ([TyVar], Type, CoAxiom Unbranched) +unwrapNewTyConEtad_maybe (AlgTyCon { algTcRhs = NewTyCon { nt_co = co, + nt_etad_rhs = (tvs,rhs) }}) + = Just (tvs, rhs, co) +unwrapNewTyConEtad_maybe _ = Nothing + isProductTyCon :: TyCon -> Bool -- True of datatypes or newtypes that have -- one, vanilla, data constructor diff --git a/compiler/types/Type.lhs b/compiler/types/Type.lhs index 6c59450aa6..94e8c24277 100644 --- a/compiler/types/Type.lhs +++ b/compiler/types/Type.lhs @@ -36,7 +36,7 @@ module Type ( mkForAllTy, mkForAllTys, splitForAllTy_maybe, splitForAllTys, mkPiKinds, mkPiType, mkPiTypes, - applyTy, applyTys, applyTysD, dropForAlls, + applyTy, applyTys, applyTysD, applyTysX, dropForAlls, mkNumLitTy, isNumLitTy, mkStrLitTy, isStrLitTy, @@ -575,11 +575,10 @@ newTyConInstRhs :: TyCon -> [Type] -> Type -- arguments, using an eta-reduced version of the @newtype@ if possible. -- This requires tys to have at least @newTyConInstArity tycon@ elements. newTyConInstRhs tycon tys - = ASSERT2( equalLength tvs tys1, ppr tycon $$ ppr tys $$ ppr tvs ) - mkAppTys (substTyWith tvs tys1 ty) tys2 + = ASSERT2( tvs `leLength` tys, ppr tycon $$ ppr tys $$ ppr tvs ) + applyTysX tvs rhs tys where - (tvs, ty) = newTyConEtadRhs tycon - (tys1, tys2) = splitAtList tvs tys + (tvs, rhs) = newTyConEtadRhs tycon \end{code} @@ -824,13 +823,22 @@ applyTysD doc orig_fun_ty arg_tys = substTyWith (take n_args tvs) arg_tys (mkForAllTys (drop n_args tvs) rho_ty) | otherwise -- Too many type args - = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty ) -- Zero case gives infinite loop! + = ASSERT2( n_tvs > 0, doc $$ ppr orig_fun_ty $$ ppr arg_tys ) -- Zero case gives infinite loop! applyTysD doc (substTyWith tvs (take n_tvs arg_tys) rho_ty) (drop n_tvs arg_tys) where (tvs, rho_ty) = splitForAllTys orig_fun_ty - n_tvs = length tvs + n_tvs = length tvs n_args = length arg_tys + +applyTysX :: [TyVar] -> Type -> [Type] -> Type +-- applyTyxX beta-reduces (/\tvs. body_ty) arg_tys +applyTysX tvs body_ty arg_tys + = ASSERT2( length arg_tys >= n_tvs, ppr tvs $$ ppr body_ty $$ ppr arg_tys ) + mkAppTys (substTyWith tvs (take n_tvs arg_tys) body_ty) + (drop n_tvs arg_tys) + where + n_tvs = length tvs \end{code} diff --git a/testsuite/tests/indexed-types/should_fail/T9580.hs b/testsuite/tests/indexed-types/should_fail/T9580.hs new file mode 100644 index 0000000000..de5455f493 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T9580.hs @@ -0,0 +1,7 @@ +module T9580 where + +import T9580a +import Data.Coerce + +foo :: Dimensional Int Double -> Double +foo x = coerce x diff --git a/testsuite/tests/indexed-types/should_fail/T9580.stderr b/testsuite/tests/indexed-types/should_fail/T9580.stderr new file mode 100644 index 0000000000..19ceefb0ff --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T9580.stderr @@ -0,0 +1,10 @@ +[1 of 2] Compiling T9580a ( T9580a.hs, T9580a.o ) +[2 of 2] Compiling T9580 ( T9580.hs, T9580.o ) + +T9580.hs:7:9: + Could not coerce from ‘Dimensional Int Double’ to ‘Double’ + because the data constructor ‘T9580a.Quantity'’ + of newtype ‘Dimensional Int v’ is not in scope + arising from a use of ‘coerce’ + In the expression: coerce x + In an equation for ‘foo’: foo x = coerce x diff --git a/testsuite/tests/indexed-types/should_fail/T9580a.hs b/testsuite/tests/indexed-types/should_fail/T9580a.hs new file mode 100644 index 0000000000..578c8bafb8 --- /dev/null +++ b/testsuite/tests/indexed-types/should_fail/T9580a.hs @@ -0,0 +1,5 @@ +{-# LANGUAGE KindSignatures, TypeFamilies #-} +module T9580a( Dimensional ) where + +data family Dimensional var :: * -> * +newtype instance Dimensional Int v = Quantity' v diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T index 2862f1e854..f06060efd0 100644 --- a/testsuite/tests/indexed-types/should_fail/all.T +++ b/testsuite/tests/indexed-types/should_fail/all.T @@ -128,4 +128,5 @@ test('T9357', normal, compile_fail, ['']) test('T9371', normal, compile_fail, ['']) test('T9433', normal, compile_fail, ['']) test('BadSock', normal, compile_fail, ['']) +test('T9580', normal, multimod_compile_fail, ['T9580', '']) diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr index 5bb9210a13..b95b4cea67 100644 --- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr +++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr @@ -33,7 +33,8 @@ TcCoercibleFail.hs:16:8: TcCoercibleFail.hs:18:8: Could not coerce from ‘Int’ to ‘Down Int’ - because the constructor of ‘Down’ is not imported + because the data constructor ‘Data.Ord.Down’ + of newtype ‘Down’ is not in scope arising from a use of ‘coerce’ In the expression: coerce In the expression: coerce $ one :: Down Int |