Commit ae4c8ca4 authored by mnislaih's avatar mnislaih
Browse files

Clean up & comments

parent 87c1c2ff
......@@ -376,9 +376,27 @@ repPrim t = rep where
| t == tVarPrimTyCon = "<tVar>"
| otherwise = showSDoc (char '<' <> ppr t <> char '>')
where build ww = unsafePerformIO $ withArray ww (peek . castPtr)
-----------------------------------
-- Type Reconstruction
-----------------------------------
{-
Type Reconstruction is type inference done on heap closures.
The algorithm walks the heap generating a set of equations, which
are solved with syntactic unification.
A type reconstruction equation looks like:
<datacon reptype> = <actual heap contents>
The full equation set is generated by traversing all the subterms, starting
from a given term.
The only difficult part is that newtypes are only found in the lhs of equations.
Right hand sides are missing them. We can either (a) drop them from the lhs, or
(b) reconstruct them in the rhs when possible.
The function congruenceNewtypes takes a shot at (b)
-}
-- The Type Reconstruction monad
type TR a = TcM a
......@@ -393,88 +411,11 @@ runTR hsc_env c = do
trIO :: IO a -> TR a
trIO = liftTcM . ioToTcRn
addConstraint :: TcType -> TcType -> TR ()
addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType
{-
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 = go True
where
go rewriteRHS lhs rhs
-- TyVar lhs inductive case
| Just tv <- getTyVar_maybe lhs
= recoverM (return (lhs,rhs)) $ do
Indirect ty_v <- readMetaTyVar tv
(lhs', rhs') <- go rewriteRHS ty_v rhs
writeMutVar (metaTvRef tv) (Indirect lhs')
return (lhs, rhs')
-- TyVar rhs inductive case
| Just tv <- getTyVar_maybe rhs
= recoverM (return (lhs,rhs)) $ do
Indirect ty_v <- readMetaTyVar tv
(lhs', rhs') <- go rewriteRHS lhs ty_v
writeMutVar (metaTvRef tv) (Indirect rhs')
return (lhs', rhs)
-- FunTy inductive case
| Just (l1,l2) <- splitFunTy_maybe lhs
, Just (r1,r2) <- splitFunTy_maybe rhs
= do (l2',r2') <- go True l2 r2
(l1',r1') <- go False 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 = do
let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l)
then (tycon_r, rewrite tycon_r lhs)
else (tycon_l, args_l)
(tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r)
then (tycon_l, rewrite tycon_l rhs)
else (tycon_r, args_r)
(args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r'
return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'')
| otherwise = return (lhs,rhs)
where rewrite newtyped_tc lame_tipe
| (tvs, tipe) <- newTyConRep newtyped_tc
= case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of
Just subst -> substTys subst (map mkTyVarTy tvs)
otherwise -> panic "congruenceNewtypes: Can't unify a newtype"
liftTcM = id
newVar :: Kind -> TR TcTyVar
newVar = liftTcM . newFlexiTyVar
liftTcM = id
-- | Returns the instantiated type scheme ty', and the substitution sigma
-- such that sigma(ty') = ty
instScheme :: Type -> TR (TcType, TvSubst)
......@@ -482,6 +423,12 @@ instScheme ty | (tvs, rho) <- tcSplitForAllTys ty = liftTcM$ do
(tvs',theta,ty') <- tcInstType (mapM tcInstTyVar) ty
return (ty', zipTopTvSubst tvs' (mkTyVarTys tvs))
addConstraint :: TcType -> TcType -> TR ()
addConstraint t1 t2 = congruenceNewtypes t1 t2 >>= uncurry unifyType
-- Type & Term reconstruction
cvObtainTerm :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Term
cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
tv <- liftM mkTyVarTy (newVar argTypeKind)
......@@ -553,11 +500,10 @@ cvObtainTerm hsc_env force mb_ty hval = runTR hsc_env $ do
, ptext SLIT("reOrderTerms") $$ (ppr pointed $$ ppr unpointed))
head unpointed : reOrderTerms pointed (tail unpointed) tys
-- Strict application of f at index i
appArr f (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of
(# e #) -> f e
-- Fast, breadth-first version of obtainTerm that deals only with type reconstruction
cvReconstructType :: HscEnv -> Bool -> Maybe Type -> HValue -> IO Type
cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do
tv <- liftM mkTyVarTy (newVar argTypeKind)
......@@ -602,6 +548,84 @@ cvReconstructType hsc_env force mb_ty hval = runTR hsc_env $ do
otherwise -> return []
-- 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 = go True
where
go rewriteRHS lhs rhs
-- TyVar lhs inductive case
| Just tv <- getTyVar_maybe lhs
= recoverM (return (lhs,rhs)) $ do
Indirect ty_v <- readMetaTyVar tv
(lhs', rhs') <- go rewriteRHS ty_v rhs
writeMutVar (metaTvRef tv) (Indirect lhs')
return (lhs, rhs')
-- TyVar rhs inductive case
| Just tv <- getTyVar_maybe rhs
= recoverM (return (lhs,rhs)) $ do
Indirect ty_v <- readMetaTyVar tv
(lhs', rhs') <- go rewriteRHS lhs ty_v
writeMutVar (metaTvRef tv) (Indirect rhs')
return (lhs', rhs)
-- FunTy inductive case
| Just (l1,l2) <- splitFunTy_maybe lhs
, Just (r1,r2) <- splitFunTy_maybe rhs
= do (l2',r2') <- go True l2 r2
(l1',r1') <- go False 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 = do
let (tycon_l',args_l') = if isNewTyCon tycon_r && not(isNewTyCon tycon_l)
then (tycon_r, rewrite tycon_r lhs)
else (tycon_l, args_l)
(tycon_r',args_r') = if rewriteRHS && isNewTyCon tycon_l && not(isNewTyCon tycon_r)
then (tycon_l, rewrite tycon_l rhs)
else (tycon_r, args_r)
(args_l'', args_r'') <- unzip `liftM` zipWithM (go rewriteRHS) args_l' args_r'
return (mkTyConApp tycon_l' args_l'', mkTyConApp tycon_r' args_r'')
| otherwise = return (lhs,rhs)
where rewrite newtyped_tc lame_tipe
| (tvs, tipe) <- newTyConRep newtyped_tc
= case tcUnifyTys (const BindMe) [tipe] [lame_tipe] of
Just subst -> substTys subst (map mkTyVarTy tvs)
otherwise -> panic "congruenceNewtypes: Can't unify a newtype"
------------------------------------------------------------------------------------
isMonomorphic ty | (tvs, ty') <- splitForAllTys ty
= null tvs && (isEmptyVarSet . tyVarsOfType) ty'
......@@ -612,6 +636,10 @@ 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 (Array _ _ ptrs#) (I# i#) = case indexArray# ptrs# i# of
(# e #) -> f e
zonkTerm :: Term -> TcM Term
zonkTerm = foldTerm idTermFoldM {
fTerm = \ty dc v tt -> sequence tt >>= \tt ->
......@@ -625,53 +653,4 @@ zonkTerm = foldTerm idTermFoldM {
-- Generalize the type: find all free tyvars and wrap in the appropiate ForAll.
sigmaType ty = mkForAllTys (varSetElems$ tyVarsOfType (dropForAlls ty)) ty
{-
Example of Type Reconstruction
--------------------------------
Suppose we have an existential type such as
data Opaque = forall a. Opaque a
And we have a term built as:
t = Opaque (map Just [[1,1],[2,2]])
The type of t as far as the typechecker goes is t :: Opaque
If we seq the head of t, we obtain:
t - O (_1::a)
seq _1 ()
t - O ( (_3::b) : (_4::[b]) )
seq _3 ()
t - O ( (Just (_5::c)) : (_4::[b]) )
At this point, we know that b = (Maybe c)
seq _5 ()
t - O ( (Just ((_6::d) : (_7::[d]) )) : (_4::[b]) )
At this point, we know that c = [d]
seq _6 ()
t - O ( (Just (1 : (_7::[d]) )) : (_4::[b]) )
At this point, we know that d = Integer
The fully reconstructed expressions, with propagation, would be:
t - O ( (Just (_5::c)) : (_4::[Maybe c]) )
t - O ( (Just ((_6::d) : (_7::[d]) )) : (_4::[Maybe [d]]) )
t - O ( (Just (1 : (_7::[Integer]) )) : (_4::[Maybe [Integer]]) )
For reference, the type of the thing inside the opaque is
map Just [[1,1],[2,2]] :: [Maybe [Integer]]
NOTE: (Num t) contexts have been manually replaced by Integer for clarity
-}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment