patch applied (ghc): cvReconstructType: a faster, types-only version of cvObtainTerm

[Pepe Iborra]

>
> I read through the code a bit more (while we were chatting on  
> IRC).  I think I understand more or less what's going on, here's a  
> couple more comments:
>
> I'd write search like this:
>
> +  search stop combine []         = return ()
> +  search stop combine ((t,a):jj) = do
> +      pairs <- go t a
> +      unlessM stop $ search stop combine (jj `combine` pairs)
>
> that's about the same amount of code, but I eliminated one fmap,  
> one >>= and one (.), and it's a whole lot easier to read (for me at  
> least!).
>

When one of the Simons says that he is having trouble reading your  
code, you ought to listen!

Now that you are looking at the type reconstruction stuff, it cannot  
hurt for me to write some ideas down.
As you surely have seen, type reconstruction is pretty easy. The only  
tricky bits are:

- What congruenceNewTypes does. Don't ask me to explain it; the only  
hope to understand it (even for myself) is go through the simple  
typing rules in the report and try to make sense (supposing that  
congruenceNewTypes really implements those faithfully).
- Being careful on the order of the unification steps, or  
congruenceNewTypes will stop working
- Not introducing thunks in some step, or go will stop working.
- Dealing with the substitutions before & after the reconstruction.

The algorithm, apart from congruenceNewtypes, is entirely  
straightforward, doing just what one would expect. Wall the subterm  
tree, generate a constraint in each step down, and solve them. There  
is an clear example about that in the report sec. 4.3, fig. 5 (btw I  
found some embarrassing typos and will upload an updated version soon).
Since TcM solves constraints as they are added, this is why the order  
is important.
Other than that, you have to take care of the small details like  
extra args in the signature.

When you add term construction into the mix, as in cvObtainTerm,  
things get more messy. And there is the optimization to replace  
unification for matching when possible, because as you pointed out in  
IRC, cvObtainTerm cannot stop until it has walked the entire subterm  
tree due to thunks needing to be typed.

> I noticed that you always call search with (++) as the combine  
> argument.  Might want to specialise there.

Damn. I first produced a textbook version of general search, then  
chose (++) for a bfs strategy, checked that it worked, and then  
stopped thinking and ran for beers to celebrate :)

>
> You're doing a breadth-first search by appending to the end of the  
> list; this will be a performance problem if the list gets long.  I  
> suggest using Data.Sequence instead, or roll a separate Deque type  
> (using the two-lists trick, for example, I did something similar in  
> InteractiveEval.BoundedList).

I'll just go for Data.Sequence :)
It's really nice that we can use all the libraries now, thanks to  
compat right?

Cheers
pepe