Commit 0aaf812e authored by Simon Peyton Jones's avatar Simon Peyton Jones

Clean up Coercible handling, and interaction of data families with newtypes

This patch fixes Trac #9580, in which the Coercible machinery succeeded
even though the relevant data constructor was not in scope.

As usual I got dragged into a raft of refactoring changes,
all for the better.

* Delete TcEvidence.coercionToTcCoercion (now unused)

* Move instNewTyConTF_maybe, instNewTyCon_maybe to FamInst,
  and rename them to tcInstNewTyConTF_maybe, tcInstNewTyCon
  (They both return TcCoercions.)

* tcInstNewTyConTF_maybe also gets more convenient type,
  which improves TcInteract.getCoercibleInst

* Define FamInst.tcLookupDataFamInst, and use it in TcDeriv,
  (as well as in tcInstNewTyConTF_maybe)

* Improve error report for Coercible errors, when data familes
  are involved  Another use of tcLookupDataFamInst

* In TcExpr.tcTagToEnum, use tcLookupDataFamInst to replace
  local hacky code

* Fix Coercion.instNewTyCon_maybe and Type.newTyConInstRhs to deal
  with eta-reduced newtypes, using
  (new) Type.unwrapNewTyConEtad_maybe and (new) Type.applyTysX

Some small refactoring of TcSMonad.matchFam.
parent 24e51b01
......@@ -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
......
......@@ -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}
......
......@@ -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]
......
......@@ -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
......
......@@ -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}
%************************************************************************
......
......@@ -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}
......
......@@ -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,
......
......@@ -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 })
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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}
......
module T9580 where
import T9580a
import Data.Coerce
foo :: Dimensional Int Double -> Double
foo x = coerce x