[GHC] #1330: Church2 test gives a rather confusing error with the HEAD

[GHC]

#1330: Church2 test gives a rather confusing error with the HEAD
----------------------------------------+-----------------------------------
    Reporter:  igloo                    |        Owner:         
        Type:  bug                      |       Status:  new    
    Priority:  normal                   |    Milestone:  6.8    
   Component:  Compiler (Type checker)  |      Version:  6.7    
    Severity:  normal                   |   Resolution:         
    Keywords:                           |   Difficulty:  Unknown
          Os:  Unknown                  |     Testcase:  Church2
Architecture:  Unknown                  |  
----------------------------------------+-----------------------------------
Comment (by simonpj):

 Sigh.  This a great example of why typechecking for impredicative
 polymorphism is so darn tricky. Here is what is happening.  The call `n
 (mul m) n1` means that we try to check `(mul m)` expecting it to have type
 `CNat -> CNat`.  Not knowing (yet) what type to instantiate `mul` to, we
 instantiate it to type `box(a)`.  So now we are faced with the task of
 checking
 {{{
   box(a) -> box(a)  <=  CNat -> CNat
 }}}
 If you follow through the rules of Fig 3
 of[http://research.microsoft.com/~simonpj/papers/boxy/boxy-icfp.pdf the
 paper], we find that, from the ''argument'' side of the arrows we must
 equate `box(a)` and `CNat`.  That leaves us with the following problem:
 {{{
   box(CNat) -> box(CNat)   <=   CNat -> CNat
 }}}
 Looking now at the ''result''side of the arrow we get
 {{{
   box(CNat)   <=   CNat
 }}}
 You might think that this is obviously possible, but rule SKOL says to
 instantiate the `CNat` onn the right; and that soon leads the reported
 mis-match.

 The trouble is that GHC does as much zonking as possible before reporting
 the error, and does not show the boxes.  Result: we display two identical-
 looking types.

 I'm not sure how to fix this, and in any case I'm unhappy with the
 impredicative-polymoprhism story.  So I'm going to leave this as one more
 reason why the current story is unsatisfactory, and hope that Stephanie
 and Dimitrios eventually show the way forward!

 Meanwhile, better make this an expected failure.

 Simon

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/1330>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
-------------- next part --------------
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs at haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs