91 | | === Type reconstruction === |
92 | | `obtainTerm` recursively traverses all the closures that conform a term. Indirections are followed and suspensions are optionally forced. The only problem here is dealing with types. DataCons can have polymorphic types which we would want to instantiate, so the knowledge of the datacon only is not enough. There are two other sources of type information: |
93 | | 1. The typechecker, via the `Id` argument to `obtainTerm`. |
94 | | 2. The concrete types of the subterms, if they are sufficiently evaluated. |
95 | | |
96 | | The process followed to reconstruct the types of a value as much as possible is: |
97 | | |
98 | | 1. obtain the subTerms of the value recursively calling `obtainTerm` with the available type info (dataCon plus typechecker), discovering new type info in the process. |
99 | | 2. refine the type of the value. This is accomplished with a step of unification between (1) and (2) above, and matching the result with the type of the datacon, obtaining the tyvars, which are used to instantiate. This step obtains the most concrete type. |
100 | | * Note that tyvars need renaming to avoid collisions. |
101 | | 3. refine the type of the subterms (inductively) with the reconstructed type. |
| 91 | === Recovering non-pointers === |
| 92 | This happens at `RtClosureInspect.extractUnboxed` and is a bit weak, it might potentially break in some architectures. |
| 108 | |
| 109 | === Type reconstruction === |
| 110 | Type reconstruction is the process of recovering the full type of a closure which has a polymorphic dataCon. |
| 111 | |
| 112 | The problem is approached as a simplified case of type inference. The set of constraints come from the typechecker and from the concrete types of the children of the closure, if they are evaluated. Constraints are are generated and unified with the previous set, ultimately generating the desired substitution. |
| 113 | |
| 114 | The only tricky issue is that newtypes are gone in the heap representation, so one needs to consider additional equations when doing unification, very similar to the coercions (:=:) of System Fc. For instance, the newtype: |
| 115 | {{{ |
| 116 | newtype MkT a = MkT [a] |
| 117 | }}} |
| 118 | |
| 119 | induces an equivalence class: |
| 120 | {{{ |
| 121 | MkT a :=: [a] |
| 122 | }}} |
| 123 | |
| 124 | This can be quite tricky to solve if done in full generality, as it amounts to unification modulo a set of equations which is known to be undecidible. The closure viewer uses the simpler trick of scanning every constraint lhs for newtypes and adjusting the rhs correspondingly. This simple trick seems to do it (see `congruenceNewtypes` at [[GhcFile(compiler/ghci/RtClosureInspect.hs)]]). |
| 125 | |
| 126 | |
| 128 | Often it is not possible to reconstruct the most concrete type, because children of a value are suspended. When this happens we have a value with polymorphic type, and this is a problem for two reasons. First, for the user, who cannot interact with the value in the usual way. Second, for ghci, because it does not deal well with tyvars in the type of values. |
| 129 | |
| 130 | Ideally, we want to lift this restriction on ghci some day. For now, the tyvars are instantiated to a family of dummy types, indexed by kind arity, which live in GHC.Base: `Unknown`, `Unknown1`,`Unknown2`, etc. |
| 131 | |
| 141 | |
| 142 | === Type Refinement === |
| 143 | `InteractiveUI.pprintClosure` has some smartness in to update the type of a value as it is refined by forcing evaluation. As an example, look at the following (allegedly extreme) debugging session snippet: |
| 144 | |
| 145 | {{{ |
| 146 | Local bindings in scope: |
| 147 | r :: a |
| 148 | |
| 149 | Core.hs:335:35-49> :t r |
| 150 | r :: GHC.Base.Unknown |
| 151 | |
| 152 | Core.hs:335:35-49> :p r |
| 153 | r = (_t1::a) |
| 154 | |
| 155 | Core.hs:335:35-49> seq _t1 () |
| 156 | () |
| 157 | |
| 158 | Core.hs:335:35-49> :p r |
| 159 | r = :-> (_t2::a) (_t3::a) |
| 160 | |
| 161 | Core.hs:335:35-49> :t r |
| 162 | r :: RuleG GHC.Base.Unknown |
| 163 | |
| 164 | Core.hs:335:35-49> seq _t2 () |
| 165 | () |
| 166 | |
| 167 | Core.hs:335:35-49> :p r |
| 168 | r = :-> S (_t4::b (GT_ a b c)) (_t5::GT_ a b c) |
| 169 | |
| 170 | Core.hs:335:35-49> :t r |
| 171 | r :: RuleG (GT_ GHC.Base.Unknown |
| 172 | GHC.Base.Unknown1 |
| 173 | GHC.Base.Unknown) |
| 174 | |
| 175 | Core.hs:335:35-49> seq _t4 () |
| 176 | () |
| 177 | |
| 178 | Core.hs:335:35-49> :p r |
| 179 | r = :-> (S T "+" [(_t6::GT_ a TermST b), GenVar 1]) (_t7::GT_ a TermST b) |
| 180 | |
| 181 | Core.hs:335:35-49> :t r |
| 182 | r :: RuleG (GT_ GHC.Base.Unknown TermST GHC.Base.Unknown) |
| 183 | }}} |
| 184 | |
| 185 | Note how the type of the binding `r` gets updated during the debugging session. |