[GHC] #5678: Unexpected cryptic GADT type error

[GHC]

#5678: Unexpected cryptic GADT type error
---------------------------------+------------------------------------------
  Reporter:  mikhail.vorozhtsov  |          Owner:                  
      Type:  bug                 |         Status:  closed          
  Priority:  normal              |      Milestone:                  
 Component:  Compiler            |        Version:  7.3             
Resolution:  invalid             |       Keywords:                  
  Testcase:                      |      Blockedby:                  
Difficulty:                      |             Os:  Unknown/Multiple
  Blocking:                      |   Architecture:  Unknown/Multiple
   Failure:  None/Unknown        |  
---------------------------------+------------------------------------------

Comment(by mikhail.vorozhtsov):

 Wow, that's really confusing. Is the "a" in "n a" is the same as in "x ::
 G a"? That makes no sense to me. Would it be right to say that GHC "dumbs"
 itself down a bit when it sees a GADT (perhaps in order to guarantee
 termination of the type inferencing)? Because it sure has no problem with
 {{{
 ok :: (Functor m, Monad m) => m ()
 ok = void $ case x of D -> return 3
   where x :: D
         x = undefined
 }}}
 and I can't see how "return 3" becomes any more ambiguous when the "x"
 changes its type.

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/5678#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler