+-- 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 -> IO (Maybe TvSubst)
+improveRTTIType hsc_env _ty rtti_ty = runTR_maybe hsc_env $ do
+ traceTR (text "improveRttiType" <+> fsep [ppr _ty, ppr rtti_ty])
+ (ty_tvs, _, _) <- tcInstType return ty
+ (ty_tvs', _, ty') <- tcInstType (mapM tcInstTyVar) ty
+ (_, _, rtti_ty') <- tcInstType (mapM tcInstTyVar) (sigmaType rtti_ty)
+ _ <- getConstraints(unifyType rtti_ty' ty')
+ tvs1_contents <- zonkTcTyVars ty_tvs'
+ let subst = (uncurry zipTopTvSubst . unzip)
+ [(tv,ty) | (tv,ty) <- zip ty_tvs tvs1_contents
+ , getTyVar_maybe ty /= Just tv
+ --, not(isTyVarTy ty)
+ ]
+ return subst
+ where ty = sigmaType _ty
+
+myDataConInstArgTys :: DataCon -> [Type] -> [Type]
+myDataConInstArgTys dc args
+ | null (dataConExTyVars dc) && null (dataConEqTheta dc) = dataConInstArgTys dc args
+ | otherwise = dataConRepArgTys dc
+
+mydataConType :: DataCon -> Type
+-- ^ Custom version of DataCon.dataConUserType where we
+-- - remove the equality constraints
+-- - use the representation types for arguments, including dictionaries
+-- - keep the original result type
+mydataConType dc
+ = mkForAllTys ((univ_tvs `minusList` map fst eq_spec) ++ ex_tvs) $
+ mkFunTys arg_tys $
+ res_ty
+ where univ_tvs = dataConUnivTyVars dc
+ ex_tvs = dataConExTyVars dc
+ eq_spec = dataConEqSpec dc
+ arg_tys = [case a of
+ PredTy p -> predTypeRep p
+ _ -> a
+ | a <- dataConRepArgTys dc]
+ res_ty = dataConOrigResTy dc
+
+isRefType :: Type -> Bool
+isRefType ty
+ | Just (tc, _) <- tcSplitTyConApp_maybe ty' = isRefTyCon tc
+ | otherwise = False
+ where ty'= repType ty
+
+isRefTyCon :: TyCon -> Bool
+isRefTyCon tc = tc `elem` [mutVarPrimTyCon, mVarPrimTyCon, tVarPrimTyCon]
+
+-- Soundness checks
+--------------------
+{-
+This is not formalized anywhere, so hold to your seats!
+RTTI in the presence of newtypes can be a tricky and unsound business.
+
+Example:
+~~~~~~~~~
+Suppose we are doing RTTI for a partially evaluated
+closure t, the real type of which is t :: MkT Int, for
+
+ newtype MkT a = MkT [Maybe a]
+
+The table below shows the results of RTTI and the improvement
+calculated for different combinations of evaluatedness and :type t.
+Regard the two first columns as input and the next two as output.
+
+ # | t | :type t | rtti(t) | improv. | result
+ ------------------------------------------------------------
+ 1 | _ | t b | a | none | OK
+ 2 | _ | MkT b | a | none | OK
+ 3 | _ | t Int | a | none | OK
+
+ If t is not evaluated at *all*, we are safe.
+
+ 4 | (_ : _) | t b | [a] | t = [] | UNSOUND
+ 5 | (_ : _) | MkT b | MkT a | none | OK (compensating for the missing newtype)
+ 6 | (_ : _) | t Int | [Int] | t = [] | UNSOUND
+
+ If a is a minimal whnf, we run into trouble. Note that
+ row 5 above does newtype enrichment on the ty_rtty parameter.
+
+ 7 | (Just _:_)| t b |[Maybe a] | t = [], | UNSOUND
+ | | | b = Maybe a|
+
+ 8 | (Just _:_)| MkT b | MkT a | none | OK
+ 9 | (Just _:_)| t Int | FAIL | none | OK
+
+ And if t is any more evaluated than whnf, we are still in trouble.
+ Because constraints are solved in top-down order, when we reach the
+ Maybe subterm what we got is already unsound. This explains why the
+ row 9 fails to complete.
+
+ 10 | (Just _:_)| t Int | [Maybe a] | FAIL | OK
+ 11 | (Just 1:_)| t Int | [Maybe Int] | FAIL | OK
+
+ We can undo the failure in row 9 by leaving out the constraint
+ coming from the type signature of t (i.e., the 2nd column).
+ Note that this type information is still used
+ to calculate the improvement. But we fail
+ when trying to calculate the improvement, as there is no unifier for
+ t Int = [Maybe a] or t Int = [Maybe Int].
+
+
+ Another set of examples with t :: [MkT (Maybe Int)] \equiv [[Maybe (Maybe Int)]]
+
+ # | t | :type t | rtti(t) | improvement | result
+ ---------------------------------------------------------------------
+ 1 |(Just _:_) | [t (Maybe a)] | [[Maybe b]] | t = [] |
+ | | | | b = Maybe a |
+
+The checks:
+~~~~~~~~~~~
+Consider a function obtainType that takes a value and a type and produces
+the Term representation and a substitution (the improvement).
+Assume an auxiliar rtti' function which does the actual job if recovering
+the type, but which may produce a false type.
+
+In pseudocode:
+
+ rtti' :: a -> IO Type -- Does not use the static type information
+
+ obtainType :: a -> Type -> IO (Maybe (Term, Improvement))
+ obtainType v old_ty = do
+ rtti_ty <- rtti' v
+ if monomorphic rtti_ty || (check rtti_ty old_ty)
+ then ...
+ else return Nothing
+ where check rtti_ty old_ty = check1 rtti_ty &&
+ check2 rtti_ty old_ty
+
+ check1 :: Type -> Bool
+ check2 :: Type -> Type -> Bool
+
+Now, if rtti' returns a monomorphic type, we are safe.
+If that is not the case, then we consider two conditions.
+
+
+1. To prevent the class of unsoundness displayed by
+ rows 4 and 7 in the example: no higher kind tyvars
+ accepted.
+
+ check1 (t a) = NO
+ check1 (t Int) = NO
+ check1 ([] a) = YES
+
+2. To prevent the class of unsoundness shown by row 6,
+ the rtti type should be structurally more
+ defined than the old type we are comparing it to.
+ check2 :: NewType -> OldType -> Bool
+ check2 a _ = True
+ check2 [a] a = True
+ check2 [a] (t Int) = False
+ check2 [a] (t a) = False -- By check1 we never reach this equation
+ check2 [Int] a = True
+ check2 [Int] (t Int) = True
+ check2 [Maybe a] (t Int) = False
+ check2 [Maybe Int] (t Int) = True
+ check2 (Maybe [a]) (m [Int]) = False
+ check2 (Maybe [Int]) (m [Int]) = True
+
+-}
+
+check1 :: Type -> Bool
+check1 ty | (tvs, _, _) <- tcSplitSigmaTy ty = not $ any isHigherKind (map tyVarKind tvs)
+ where
+ isHigherKind = not . null . fst . splitKindFunTys
+
+check2 :: Type -> Type -> Bool
+check2 sigma_rtti_ty sigma_old_ty
+ | Just (_, rttis) <- tcSplitTyConApp_maybe rtti_ty
+ = case () of
+ _ | Just (_,olds) <- tcSplitTyConApp_maybe old_ty
+ -> and$ zipWith check2 rttis olds
+ _ | Just _ <- splitAppTy_maybe old_ty
+ -> isMonomorphicOnNonPhantomArgs rtti_ty
+ _ -> True
+ | otherwise = True
+ where (_, _ , rtti_ty) = tcSplitSigmaTy sigma_rtti_ty
+ (_, _ , old_ty) = tcSplitSigmaTy sigma_old_ty
+