@@ -40,14 +40,8 @@ elabRewrite elab ist fc Nothing rule sc newg
4040 Just t -> doEquiv elab fc t sc
4141 solve
4242 -}
43−elabRewrite elab ist fc Nothing rule sc newg
44− = elabRewrite elab ist fc (Just (sUN "rewrite__impl")) rule sc newg
45−elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
46− = do substfn <- case lookupTyName substfn_in (tt_ctxt ist) of
47− [(n, t)] -> return n
48− [] -> lift . tfail . NoSuchVariable $ substfn_in
49− more -> lift . tfail . CantResolveAlts $ map fst more
50− attack
43+elabRewrite elab ist fc substfn_in rule sc_in newg
44+ = do attack
5145 sc <- case newg of
5246 Nothing -> return sc_in
5347 Just t -> do
@@ -70,7 +64,8 @@ elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
7064 rname <- unique_hole (sMN 0 "replaced")
7165 case unApply ttrule of
7266 (P _ (UN q) _, [lt, rt, l, r]) | q == txt "=" ->
73− do let pred_tt = mkP (P Bound rname rt) l r g
67+ do substfn <- findSubstFn substfn_in ist lt rt
68+ let pred_tt = mkP (P Bound rname rt) l r g
7469 when (g == pred_tt) $ lift $ tfail (NoRewriting g)
7570 let pred = PLam fc rname fc Placeholder
7671 (delab ist pred_tt)
@@ -120,4 +115,17 @@ elabRewrite elab ist fc (Just substfn_in) rule sc_in newg
120115 where removeImp tm@(PImp{}) = tm { getTm = Placeholder }
121116 removeImp t = t
122117 phApps tm = tm
123−
118+
119+findSubstFn :: Maybe Name -> IState -> Type -> Type -> ElabD Name
120+findSubstFn Nothing ist lt rt
121+ | lt == rt = return (sUN "rewrite__impl")
122+ -- TODO: Find correct rewriting lemma, if it exists, and tidy up this
123+ -- error
124+ | otherwise = lift . tfail .
125+ Msg $ "Can't rewrite heterogeneous equality on types " ++
126+ show (delab ist lt) ++ " and " ++ show (delab ist rt)
127+findSubstFn (Just substfn_in) ist lt rt
128+ = case lookupTyName substfn_in (tt_ctxt ist) of
129+ [(n, t)] -> return n
130+ [] -> lift . tfail . NoSuchVariable $ substfn_in
131+ more -> lift . tfail . CantResolveAlts $ map fst more