--- | Returns the instantiated type scheme ty', and the substitution sigma
--- such that sigma(ty') = ty
-instScheme :: Type -> TR (TcType, TvSubst)
-instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
- (tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty
- return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
-
-cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
-cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
- tv <- liftM mkTyVarTy (newVar argTypeKind)
- case mb_ty of
- Nothing -> go tv tv hval >>= zonkTerm
- Just ty | isMonomorphic ty -> go ty ty hval >>= zonkTerm
- Just ty -> do
- (ty',rev_subst) <- instScheme (sigmaType ty)
- addConstraint tv ty'
- term <- go tv tv hval >>= zonkTerm
- --restore original Tyvars
- return$ mapTermType (substTy rev_subst) term
+newVar :: Kind -> TR TcType
+newVar = liftTcM . newFlexiTyVarTy
+
+type RttiInstantiation = [(TcTyVar, TyVar)]
+ -- Associates the typechecker-world meta type variables
+ -- (which are mutable and may be refined), to their
+ -- debugger-world RuntimeUnkSkol counterparts.
+ -- If the TcTyVar has not been refined by the runtime type
+ -- elaboration, then we want to turn it back into the
+ -- original RuntimeUnkSkol
+
+-- | Returns the instantiated type scheme ty', and the
+-- mapping from new (instantiated) -to- old (skolem) type variables
+-- We want this mapping just for old RuntimeUnkSkols, to avoid
+-- gratuitously changing their unique on every trip
+instScheme :: QuantifiedType -> TR (TcType, RttiInstantiation)
+instScheme (tvs, ty)
+ = liftTcM $ do { (tvs', _, subst) <- tcInstTyVars tvs
+ ; let rtti_inst = [(tv',tv) | (tv',tv) <- tvs' `zip` tvs
+ , isRuntimeUnkSkol tv]
+ ; return (substTy subst ty, rtti_inst) }
+
+applyRevSubst :: RttiInstantiation -> TR ()
+-- Apply the *reverse* substitution in-place to any un-filled-in
+-- meta tyvars. This recovers the original debugger-world variable
+-- unless it has been refined by new information from the heap
+applyRevSubst pairs = liftTcM (mapM_ do_pair pairs)
+ where
+ do_pair (tc_tv, rtti_tv)
+ = do { tc_ty <- zonkTcTyVar tc_tv
+ ; case tcGetTyVar_maybe tc_ty of
+ Just tv | isMetaTyVar tv -> writeMetaTyVar tv (mkTyVarTy rtti_tv)
+ _ -> return () }
+
+-- Adds a constraint of the form t1 == t2
+-- t1 is expected to come from walking the heap
+-- t2 is expected to come from a datacon signature
+-- Before unification, congruenceNewtypes needs to
+-- do its magic.
+addConstraint :: TcType -> TcType -> TR ()
+addConstraint actual expected = do
+ traceTR (text "add constraint:" <+> fsep [ppr actual, equals, ppr expected])
+ recoverTR (traceTR $ fsep [text "Failed to unify", ppr actual,
+ text "with", ppr expected]) $
+ do { (ty1, ty2) <- congruenceNewtypes actual expected
+ ; _ <- captureConstraints $ unifyType ty1 ty2
+ ; return () }
+ -- TOMDO: what about the coercion?
+ -- we should consider family instances
+
+
+-- Type & Term reconstruction
+------------------------------
+cvObtainTerm :: HscEnv -> Int -> Bool -> RttiType -> HValue -> IO Term
+cvObtainTerm hsc_env max_depth force old_ty hval = runTR hsc_env $ do
+ -- we quantify existential tyvars as universal,
+ -- as this is needed to be able to manipulate
+ -- them properly
+ let quant_old_ty@(old_tvs, old_tau) = quantifyType old_ty
+ sigma_old_ty = mkForAllTys old_tvs old_tau
+ traceTR (text "Term reconstruction started with initial type " <> ppr old_ty)
+ term <-
+ if null old_tvs
+ then do
+ term <- go max_depth sigma_old_ty sigma_old_ty hval
+ term' <- zonkTerm term
+ return $ fixFunDictionaries $ expandNewtypes term'
+ else do
+ (old_ty', rev_subst) <- instScheme quant_old_ty
+ my_ty <- newVar argTypeKind
+ when (check1 quant_old_ty) (traceTR (text "check1 passed") >>
+ addConstraint my_ty old_ty')
+ term <- go max_depth my_ty sigma_old_ty hval
+ new_ty <- zonkTcType (termType term)
+ if isMonomorphic new_ty || check2 (quantifyType new_ty) quant_old_ty
+ then do
+ traceTR (text "check2 passed")
+ addConstraint new_ty old_ty'
+ applyRevSubst rev_subst
+ zterm' <- zonkTerm term
+ return ((fixFunDictionaries . expandNewtypes) zterm')
+ else do
+ traceTR (text "check2 failed" <+> parens
+ (ppr term <+> text "::" <+> ppr new_ty))
+ -- we have unsound types. Replace constructor types in
+ -- subterms with tyvars
+ zterm' <- mapTermTypeM
+ (\ty -> case tcSplitTyConApp_maybe ty of
+ Just (tc, _:_) | tc /= funTyCon
+ -> newVar argTypeKind
+ _ -> return ty)
+ term
+ zonkTerm zterm'
+ traceTR (text "Term reconstruction completed." $$
+ text "Term obtained: " <> ppr term $$
+ text "Type obtained: " <> ppr (termType term))
+ return term