summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/hsSyn/HsUtils.lhs15
-rw-r--r--compiler/typecheck/FamInst.lhs78
-rw-r--r--compiler/typecheck/TcDeriv.lhs28
-rw-r--r--compiler/typecheck/TcErrors.lhs49
-rw-r--r--compiler/typecheck/TcEvidence.lhs21
-rw-r--r--compiler/typecheck/TcExpr.lhs46
-rw-r--r--compiler/typecheck/TcInteract.lhs88
-rw-r--r--compiler/typecheck/TcSMonad.lhs19
-rw-r--r--compiler/types/Coercion.lhs6
-rw-r--r--compiler/types/FamInstEnv.lhs31
-rw-r--r--compiler/types/TyCon.lhs9
-rw-r--r--compiler/types/Type.lhs22
-rw-r--r--testsuite/tests/indexed-types/should_fail/T9580.hs7
-rw-r--r--testsuite/tests/indexed-types/should_fail/T9580.stderr10
-rw-r--r--testsuite/tests/indexed-types/should_fail/T9580a.hs5
-rw-r--r--testsuite/tests/indexed-types/should_fail/all.T1
-rw-r--r--testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr3
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