Commit b6d52294 authored by Joachim Breitner's avatar Joachim Breitner
Browse files

getCoerbileInsts: Move the two NT-unwrapping instances together

and fix the numbering in the comments. Thank to SPJ for noticing.
Nothing deep in here, just a insufficent copy’n’pasting in revision
7e78faf0. Incidentially, 7e78faf0 did a better job updating the comments
than the code :-).
parent c1336f71
...@@ -1948,7 +1948,7 @@ getCoercibleInst loc ty1 ty2 = do ...@@ -1948,7 +1948,7 @@ getCoercibleInst loc ty1 ty2 = do
ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2) ev_term <- deferTcSForAllEq Representational loc (tvs1,body1) (tvs2,body2)
return $ GenInst [] ev_term return $ GenInst [] ev_term
-- Coercible NT a (see case 4 in [Coercible Instances]) -- Coercible NT a (see case 3 in [Coercible Instances])
| Just (tc,tyArgs) <- splitTyConApp_maybe ty1, | Just (tc,tyArgs) <- splitTyConApp_maybe ty1,
Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs, Just (concTy, ntCo) <- instNewTyConTF_maybe famenv tc tyArgs,
dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon dataConsInScope rdr_env tc -- Do not look at all tyConsOfTyCon
...@@ -1960,7 +1960,19 @@ getCoercibleInst loc ty1 ty2 = do ...@@ -1960,7 +1960,19 @@ getCoercibleInst loc ty1 ty2 = do
coercionToTcCoercion ntCo `mkTcTransCo` mkTcCoVarCo local_var coercionToTcCoercion ntCo `mkTcTransCo` mkTcCoVarCo local_var
return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo) return $ GenInst (freshGoals [ct_ev]) (EvCoercion tcCo)
-- Coercible (D ty1 ty2) (D ty1' ty2') (see case 2 in [Coercible Instances]) -- 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)
-- Coercible (D ty1 ty2) (D ty1' ty2') (see case 4 in [Coercible Instances])
| Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1, | Just (tc1,tyArgs1) <- splitTyConApp_maybe ty1,
Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2, Just (tc2,tyArgs2) <- splitTyConApp_maybe ty2,
tc1 == tc2, tc1 == tc2,
...@@ -1991,18 +2003,6 @@ getCoercibleInst loc ty1 ty2 = do ...@@ -1991,18 +2003,6 @@ getCoercibleInst loc ty1 ty2 = do
tcCo = TcLetCo binds (mkTcTyConAppCo Representational tc1 arg_cos) tcCo = TcLetCo binds (mkTcTyConAppCo Representational tc1 arg_cos)
return $ GenInst (catMaybes arg_new) (EvCoercion tcCo) return $ GenInst (catMaybes arg_new) (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)
-- Cannot solve this one -- Cannot solve this one
| otherwise | otherwise
= return NoInstance = return NoInstance
......
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