Commit 335031f0 authored by Joachim Breitner's avatar Joachim Breitner
Browse files

Extend Coercible to newtype instances

This fixes: #8548
parent db3d9711
......@@ -44,7 +44,7 @@ import Unique( Unique )
import Digraph
import TyCon ( isTupleTyCon, tyConDataCons_maybe, unwrapNewTyCon_maybe )
import TyCon ( isTupleTyCon, tyConDataCons_maybe )
import TcEvidence
import TcType
import Type
......@@ -53,6 +53,7 @@ import TysWiredIn ( eqBoxDataCon, coercibleTyCon, coercibleDataCon, tupleCon )
import Id
import Class
import DataCon ( dataConWorkId )
import FamInstEnv ( instNewTyConTF_maybe )
import Name
import MkId ( seqId )
import Var
......@@ -797,12 +798,11 @@ dsEvTerm (EvCoercible (EvCoercibleTyCon tyCon evs)) = do
dsEvTerm (EvCoercible (EvCoercibleNewType lor tyCon tys v)) = do
ntEv <- dsEvTerm v
famenv <- dsGetFamInstEnvs
let Just (_, ntCo) = instNewTyConTF_maybe famenv tyCon tys
wrapInEqRCase ntEv $ \co -> do
return $ mkCoercible $
connect lor co $
mkUnbranchedAxInstCo Representational coAxiom tys
where Just (_, _, coAxiom) = unwrapNewTyCon_maybe tyCon
connect CLeft co2 co1 = mkTransCo co1 co2
return $ mkCoercible $ connect lor co ntCo
where connect CLeft co2 co1 = mkTransCo co1 co2
connect CRight co2 co1 = mkTransCo co2 (mkSymCo co1)
wrapInEqRCase :: CoreExpr -> (Coercion -> DsM CoreExpr) -> DsM CoreExpr
......
......@@ -26,6 +26,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 TcEvidence
import Outputable
......@@ -1845,8 +1846,9 @@ matchClassInst _ clas [ _k, ty1, ty2 ] loc
| clas == coercibleClass = do
traceTcS "matchClassInst for" $ ppr clas <+> ppr ty1 <+> ppr ty2 <+> text "at depth" <+> ppr (ctLocDepth loc)
rdr_env <- getGlobalRdrEnvTcS
famenv <- getFamInstEnvs
safeMode <- safeLanguageOn `fmap` getDynFlags
ev <- getCoercibleInst safeMode rdr_env loc ty1 ty2
ev <- getCoercibleInst safeMode famenv rdr_env loc ty1 ty2
traceTcS "matchClassInst returned" $ ppr ev
return ev
......@@ -1932,8 +1934,8 @@ matchClassInst inerts clas tys loc
-- See Note [Coercible Instances]
-- Changes to this logic should likely be reflected in coercible_msg in TcErrors.
getCoercibleInst :: Bool -> GlobalRdrEnv -> CtLoc -> TcType -> TcType -> TcS LookupInstResult
getCoercibleInst safeMode rdr_env loc ty1 ty2
getCoercibleInst :: Bool -> FamInstEnvs -> GlobalRdrEnv -> CtLoc -> TcType -> TcType -> TcS LookupInstResult
getCoercibleInst safeMode famenv rdr_env loc ty1 ty2
| ty1 `tcEqType` ty2
= do return $ GenInst []
$ EvCoercible (EvCoercibleRefl ty1)
......@@ -1957,21 +1959,17 @@ getCoercibleInst safeMode rdr_env loc ty1 ty2
$ EvCoercible (EvCoercibleTyCon tc1 (map snd arg_evs))
| Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
Just (_, _, _) <- unwrapNewTyCon_maybe tc,
newTyConEtadArity tc <= length tyArgs,
Just (concTy, _) <- instNewTyConTF_maybe famenv tc tyArgs,
dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
= do markDataConsAsUsed rdr_env tc
let concTy = newTyConInstRhs tc tyArgs
ct_ev <- requestCoercible loc concTy ty2
return $ GenInst (freshGoals [ct_ev])
$ EvCoercible (EvCoercibleNewType CLeft tc tyArgs (getEvTerm ct_ev))
| Just (tc,tyArgs) <- splitTyConApp_maybe ty2,
Just (_, _, _) <- unwrapNewTyCon_maybe tc,
newTyConEtadArity tc <= length tyArgs,
Just (concTy, _) <- instNewTyConTF_maybe famenv tc tyArgs,
dataConsInScope rdr_env tc -- Do noot look at all tyConsOfTyCon
= do markDataConsAsUsed rdr_env tc
let concTy = newTyConInstRhs tc tyArgs
ct_ev <- requestCoercible loc ty1 concTy
return $ GenInst (freshGoals [ct_ev])
$ EvCoercible (EvCoercibleNewType CRight tc tyArgs (getEvTerm ct_ev))
......
......@@ -28,7 +28,7 @@ module FamInstEnv (
isDominatedBy,
-- Normalisation
chooseBranch, topNormaliseType, topNormaliseType_maybe,
instNewTyConTF_maybe, chooseBranch, topNormaliseType, topNormaliseType_maybe,
normaliseType, normaliseTcApp,
-- Flattening
......@@ -855,6 +855,29 @@ 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'
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment