run <http://svn.berlios.de/viewcvs/al4nin/trunk/found-bugs/issue12-Cat.omg?rev=388&view=markup&gt; in Omega 1.4.2

on the prompt one can examine:

* Checking: n expected type: m refinement: (_d,_e), (_f,Prod *0), (_g,{blow (1+_c)t _h}), (_i,Cat), (_j,_h), (_k,{blow (1+_c)t _h}), (_l,_c), * assumptions: Nat' _c, * theorems: check> ZZ ZZ :: Cat {blow (1+_c)t _h} _h check> r r :: Thrist Cat _h _e check> :q

**** Near line: 313 column: 23 (V) different types _c != 0t (luf,0t)

Looks like Omega does not do post-facto type inference. The idea is: if the case expression

    where compiledRest = case check n of
                 Z -> check (compile r)

enters the first arm, we can retrospectively (post-facto) say that n is equal 0v, so their types must be the same too:

Equal _c 0t (in the second check> loop's context).

This type equality should allow to evaluate thus:

Cat {blow (1+_c)t _h} _h --> Cat {blow 1t _h} _h --> Cat [freshXX; _h]sh _h

(I am not completely sure why this is needed at all)

If this kind of type inference is feasible (algorithmically, complexity-wise), I do not know. Anyway I have written a text on it in the context of multi-dispatch languages, and it seems to be a sound concept.

looks like this problem can be worked around by lifting the pattern match from the "case n of" into the top-level pattern and duplicating the function for (PopN (S Z)) and (PopN (S (S n)).

It is demonstrated here:

http://svn.berlios.de/viewcvs/al4nin/trunk/purgatory/Cat.omg?rev=389&view=markup

regarding the soundness of this inference, it must be clear that the obtained information must be propagated in both directions. I think that needs quite a bit of pondering first, and may produce different function signatures (than e.g. Haskell's algorithm).

seems like Haskell monads already employ a similar concept:

http://reddit.com/r/programming/info/695es/comments/

Maybe this could be added as an extra heuristic to the two existing ones on page 57 of cklin's presentation http://865974842905851078-a-1802744773732722657-s-sites.googlegroups.com/site/chklin/research/dissertation-slides.pdf?attachauth=ANoY7cp-ezgu89vUrkkwthSS_9Bof8dAxypK5s_D6TniQNZVeho33aFxtvRRpPjQblOmKnlXwt1S69CAMjqEML-8g4IeMt-eFilpLPqnKUcznBLrVaubrytH_nFO0HJNFfaxH3HhmqLpbmQDNC9iQrAGwLXGPoKWETiPvUTaUqE6FjwUQEP0bj7a-8sO8RajC38ZTajU1eFAS-_bTN6vP5ILlU0LYgLXcw%3D%3D&attredirects=0 ?

Is there any relation at all? Can it improve inference? Do the two existing heuristics already cover post-facto?