+ , ptext (sLit "reOrderTerms") $$
+ (ppr pointed $$ ppr unpointed))
+ let (t:tt) = unpointed in t : reOrderTerms pointed tt tys
+
+ -- insert NewtypeWraps around newtypes
+ expandNewtypes = foldTerm idTermFold { fTerm = worker } where
+ worker ty dc hval tt
+ | Just (tc, args) <- tcSplitTyConApp_maybe ty
+ , isNewTyCon tc
+ , wrapped_type <- newTyConInstRhs tc args
+ , Just dc' <- tyConSingleDataCon_maybe tc
+ , t' <- worker wrapped_type dc hval tt
+ = NewtypeWrap ty (Right dc') t'
+ | otherwise = Term ty dc hval tt
+
+
+ -- Avoid returning types where predicates have been expanded to dictionaries.
+ fixFunDictionaries = foldTerm idTermFold {fSuspension = worker} where
+ worker ct ty hval n | isFunTy ty = Suspension ct (dictsView ty) hval n
+ | otherwise = Suspension ct ty hval n
+
+
+-- Fast, breadth-first Type reconstruction
+------------------------------------------
+cvReconstructType :: HscEnv -> Int -> GhciType -> HValue -> IO (Maybe Type)
+cvReconstructType hsc_env max_depth old_ty hval = runTR_maybe hsc_env $ do
+ traceTR (text "RTTI started with initial type " <> ppr old_ty)
+ let sigma_old_ty@(old_tvs, _) = quantifyType old_ty
+ new_ty <-
+ if null old_tvs
+ then return old_ty
+ else do
+ (old_ty', rev_subst) <- instScheme sigma_old_ty
+ my_ty <- newVar argTypeKind
+ when (check1 sigma_old_ty) (traceTR (text "check1 passed") >>
+ addConstraint my_ty old_ty')
+ search (isMonomorphic `fmap` zonkTcType my_ty)
+ (\(ty,a) -> go ty a)
+ (Seq.singleton (my_ty, hval))
+ max_depth
+ new_ty <- zonkTcType my_ty
+ if isMonomorphic new_ty || check2 (quantifyType new_ty) sigma_old_ty
+ then do
+ traceTR (text "check2 passed" <+> ppr old_ty $$ ppr new_ty)
+ addConstraint my_ty old_ty'
+ applyRevSubst rev_subst
+ zonkRttiType new_ty
+ else traceTR (text "check2 failed" <+> parens (ppr new_ty)) >>
+ return old_ty
+ traceTR (text "RTTI completed. Type obtained:" <+> ppr new_ty)
+ return new_ty
+ where
+-- search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
+ search _ _ _ 0 = traceTR (text "Failed to reconstruct a type after " <>
+ int max_depth <> text " steps")
+ search stop expand l d =
+ case viewl l of
+ EmptyL -> return ()
+ x :< xx -> unlessM stop $ do
+ new <- expand x
+ search stop expand (xx `mappend` Seq.fromList new) $! (pred d)
+
+ -- returns unification tasks,since we are going to want a breadth-first search
+ go :: Type -> HValue -> TR [(Type, HValue)]
+ go my_ty a = do
+ traceTR (text "go" <+> ppr my_ty)
+ clos <- trIO $ getClosureData a
+ case tipe clos of
+ Blackhole -> appArr (go my_ty) (ptrs clos) 0 -- carefully, don't eval the TSO
+ Indirection _ -> go my_ty $! (ptrs clos ! 0)
+ MutVar _ -> do
+ contents <- trIO$ IO$ \w -> readMutVar# (unsafeCoerce# a) w
+ tv' <- newVar liftedTypeKind
+ world <- newVar liftedTypeKind
+ addConstraint my_ty (mkTyConApp mutVarPrimTyCon [world,tv'])
+ return [(tv', contents)]
+ Constr -> do
+ Right dcname <- dataConInfoPtrToName (infoPtr clos)
+ traceTR (text "Constr1" <+> ppr dcname)
+ (_,mb_dc) <- tryTcErrs (tcLookupDataCon dcname)
+ case mb_dc of
+ Nothing-> do
+ -- TODO: Check this case
+ forM [0..length (elems $ ptrs clos)] $ \i -> do
+ tv <- newVar liftedTypeKind
+ return$ appArr (\e->(tv,e)) (ptrs clos) i
+
+ Just dc -> do
+ arg_tys <- getDataConArgTys dc my_ty
+ traceTR (text "Constr2" <+> ppr dcname <+> ppr arg_tys)
+ return $ [ appArr (\e-> (ty,e)) (ptrs clos) i
+ | (i,ty) <- zip [0..] (filter isPtrType arg_tys)]
+ _ -> return []
+
+-- Compute the difference between a base type and the type found by RTTI
+-- improveType <base_type> <rtti_type>
+-- The types can contain skolem type variables, which need to be treated as normal vars.
+-- In particular, we want them to unify with things.
+improveRTTIType :: HscEnv -> RttiType -> RttiType -> Maybe TvSubst
+improveRTTIType _ base_ty new_ty
+ = U.tcUnifyTys (const U.BindMe) [base_ty] [new_ty]
+
+getDataConArgTys :: DataCon -> Type -> TR [Type]
+-- Given the result type ty of a constructor application (D a b c :: ty)
+-- return the types of the arguments. This is RTTI-land, so 'ty' might
+-- not be fully known. Moreover, the arg types might involve existentials;
+-- if so, make up fresh RTTI type variables for them
+getDataConArgTys dc con_app_ty
+ = do { (_, ex_tys, _) <- instTyVars ex_tvs
+ ; let rep_con_app_ty = repType con_app_ty
+ ; ty_args <- case tcSplitTyConApp_maybe rep_con_app_ty of
+ Just (tc, ty_args) | dataConTyCon dc == tc
+ -> ASSERT( univ_tvs `equalLength` ty_args)
+ return ty_args
+ _ -> do { (_, ty_args, subst) <- instTyVars univ_tvs
+ ; let res_ty = substTy subst (dataConOrigResTy dc)
+ ; addConstraint rep_con_app_ty res_ty
+ ; return ty_args }
+ -- It is necessary to check dataConTyCon dc == tc
+ -- because it may be the case that tc is a recursive
+ -- newtype and tcSplitTyConApp has not removed it. In
+ -- that case, we happily give up and don't match
+ ; let subst = zipTopTvSubst (univ_tvs ++ ex_tvs) (ty_args ++ ex_tys)
+ ; return (substTys subst (dataConRepArgTys dc)) }
+ where
+ univ_tvs = dataConUnivTyVars dc
+ ex_tvs = dataConExTyVars dc
+
+isPtrType :: Type -> Bool
+isPtrType ty = case typePrimRep ty of
+ PtrRep -> True
+ _ -> False
+
+-- Soundness checks
+--------------------