+ | isPointed ty = ASSERT2(not(null pointed)
+ , ptext SLIT("reOrderTerms") $$
+ (ppr pointed $$ ppr unpointed))
+ head pointed : reOrderTerms (tail pointed) unpointed tys
+ | otherwise = ASSERT2(not(null unpointed)
+ , ptext SLIT("reOrderTerms") $$
+ (ppr pointed $$ ppr unpointed))
+ head unpointed : reOrderTerms pointed (tail unpointed) tys
+
+
+
+-- Fast, breadth-first Type reconstruction
+max_depth = 10 :: Int
+cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO (Maybe Type)
+cvReconstructType hsc_env force mb_ty hval = runTR_maybe hsc_env $ do
+ tv <- newVar argTypeKind
+ case mb_ty of
+ Nothing -> do search (isMonomorphic `fmap` zonkTcType tv)
+ (uncurry go)
+ [(tv, hval)]
+ max_depth
+ zonkTcType tv -- TODO untested!
+ Just ty | isMonomorphic ty -> return ty
+ Just ty -> do
+ (ty',rev_subst) <- instScheme (sigmaType ty)
+ addConstraint tv ty'
+ search (isMonomorphic `fmap` zonkTcType tv)
+ (\(ty,a) -> go ty a)
+ [(tv, hval)]
+ max_depth
+ substTy rev_subst `fmap` zonkTcType tv
+ where
+-- search :: m Bool -> ([a] -> [a] -> [a]) -> [a] -> m ()
+ search stop expand [] depth = return ()
+ search stop expand x 0 = fail$ "Failed to reconstruct a type after " ++
+ show max_depth ++ " steps"
+ search stop expand (x:xx) d = unlessM stop $ do
+ new <- expand x
+ search stop expand (xx ++ new) $! (pred d)
+
+ -- returns unification tasks,since we are going to want a breadth-first search
+ go :: Type -> HValue -> TR [(Type, HValue)]
+ go tv a = do
+ clos <- trIO $ getClosureData a
+ case tipe clos of
+ Indirection _ -> go tv $! (ptrs clos ! 0)
+ Constr -> do
+ Right dcname <- dataConInfoPtrToName (infoPtr clos)
+ (_,mb_dc) <- tryTcErrs (tcLookupDataCon dcname)
+ case mb_dc of
+ Nothing-> do
+ -- TODO: Check this case
+ vars <- replicateM (length$ elems$ ptrs clos)
+ (newVar (liftedTypeKind))
+ subTerms <- sequence [ appArr (go tv) (ptrs clos) i
+ | (i, tv) <- zip [0..] vars]
+ forM [0..length (elems $ ptrs clos)] $ \i -> do
+ tv <- newVar liftedTypeKind
+ return$ appArr (\e->(tv,e)) (ptrs clos) i
+
+ Just dc -> do
+ let extra_args = length(dataConRepArgTys dc) -
+ length(dataConOrigArgTys dc)
+ subTtypes <- mapMif (not . isMonomorphic)
+ (\t -> newVar (typeKind t))
+ (dataConRepArgTys dc)
+ -- It is vital for newtype reconstruction that the unification step
+ -- is done right here, _before_ the subterms are RTTI reconstructed
+ let myType = mkFunTys subTtypes tv
+ (signatureType,_) <- instScheme(dataConRepType dc)
+ addConstraint myType signatureType
+ return $ [ appArr (\e->(t,e)) (ptrs clos) i
+ | (i,t) <- drop extra_args $ zip [0..] subTtypes]
+ otherwise -> return []
+
+ -- This helper computes the difference between a base type t and the
+ -- improved rtti_t computed by RTTI
+ -- The main difference between RTTI types and their normal counterparts
+ -- is that the former are _not_ polymorphic, thus polymorphism must
+ -- be stripped. Syntactically, forall's must be stripped
+computeRTTIsubst ty rtti_ty =
+ -- In addition, we strip newtypes too, since the reconstructed type might
+ -- not have recovered them all
+ tcUnifyTys (const BindMe)
+ [repType' $ dropForAlls$ ty]
+ [repType' $ rtti_ty]
+-- TODO stripping newtypes shouldn't be necessary, test
+
+
+-- Dealing with newtypes
+{-
+ A parallel fold over two Type values,
+ compensating for missing newtypes on both sides.
+ This is necessary because newtypes are not present
+ in runtime, but since sometimes there is evidence
+ available we do our best to reconstruct them.
+ Evidence can come from DataCon signatures or
+ from compile-time type inference.
+ I am using the words congruence and rewriting
+ because what we are doing here is an approximation
+ of unification modulo a set of equations, which would
+ come from newtype definitions. These should be the
+ equality coercions seen in System Fc. Rewriting
+ is performed, taking those equations as rules,
+ before launching unification.
+
+ It doesn't make sense to rewrite everywhere,
+ or we would end up with all newtypes. So we rewrite
+ only in presence of evidence.
+ The lhs comes from the heap structure of ptrs,nptrs.
+ The rhs comes from a DataCon type signature.
+ Rewriting in the rhs is restricted to the result type.
+
+ Note that it is very tricky to make this 'rewriting'
+ work with the unification implemented by TcM, where
+ substitutions are 'inlined'. The order in which
+ constraints are unified is vital for this (or I am
+ using TcM wrongly).
+-}
+congruenceNewtypes :: TcType -> TcType -> TcM (TcType,TcType)
+congruenceNewtypes lhs rhs
+ -- TyVar lhs inductive case
+ | Just tv <- getTyVar_maybe lhs
+ = recoverTc (return (lhs,rhs)) $ do
+ Indirect ty_v <- readMetaTyVar tv
+ (lhs1, rhs1) <- congruenceNewtypes ty_v rhs
+ return (lhs, rhs1)
+-- FunTy inductive case
+ | Just (l1,l2) <- splitFunTy_maybe lhs
+ , Just (r1,r2) <- splitFunTy_maybe rhs
+ = do (l2',r2') <- congruenceNewtypes l2 r2
+ (l1',r1') <- congruenceNewtypes l1 r1
+ return (mkFunTy l1' l2', mkFunTy r1' r2')
+-- TyconApp Inductive case; this is the interesting bit.
+ | Just (tycon_l, args_l) <- splitNewTyConApp_maybe lhs
+ , Just (tycon_r, args_r) <- splitNewTyConApp_maybe rhs
+ , tycon_l /= tycon_r
+ = return (lhs, upgrade tycon_l rhs)
+
+ | otherwise = return (lhs,rhs)
+
+ where upgrade :: TyCon -> Type -> Type
+ upgrade new_tycon ty
+ | not (isNewTyCon new_tycon) = ty
+ | ty' <- mkTyConApp new_tycon (map mkTyVarTy $ tyConTyVars new_tycon)
+ , Just subst <- tcUnifyTys (const BindMe) [ty] [repType ty']
+ = substTy subst ty'
+ -- assumes that reptype doesn't touch tyconApp args ^^^
+
+
+--------------------------------------------------------------------------------
+-- Semantically different to recoverM in TcRnMonad
+-- recoverM retains the errors in the first action,
+-- whereas recoverTc here does not
+recoverTc recover thing = do
+ (_,mb_res) <- tryTcErrs thing
+ case mb_res of
+ Nothing -> recover
+ Just res -> return res
+
+isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
+ = null tvs && (isEmptyVarSet . tyVarsOfType) ty'
+
+mapMif :: Monad m => (a -> Bool) -> (a -> m a) -> [a] -> m [a]
+mapMif pred f xx = sequence $ mapMif_ pred f xx
+mapMif_ pred f [] = []
+mapMif_ pred f (x:xx) = (if pred x then f x else return x) : mapMif_ pred f xx
+
+unlessM condM acc = condM >>= \c -> unless c acc
+
+-- Strict application of f at index i
+appArr f a@(Array _ _ ptrs#) i@(I# i#) = ASSERT (i < length(elems a))
+ case indexArray# ptrs# i# of
+ (# e #) -> f e