Re: [GHC] #9918: GHC chooses an instance between two overlapping, but cannot resolve a clause within the similar closed type family

22 Dec 2014

      #9918: GHC chooses an instance between two overlapping, but cannot resolve a
clause within the similar closed type family
-------------------------------------+-------------------------------------
              Reporter:  qnikst      |            Owner:
                  Type:  bug         |           Status:  new
              Priority:  normal      |        Milestone:
             Component:  Compiler    |          Version:  7.8.3
            Resolution:              |         Keywords:
      Operating System:              |     Architecture:  Unknown/Multiple
  Unknown/Multiple                   |       Difficulty:  Unknown
       Type of failure:              |       Blocked By:
  None/Unknown                       |  Related Tickets:
             Test Case:              |
              Blocking:              |
Differential Revisions:              |
-------------------------------------+-------------------------------------
Changes (by simonpj):

 * cc: goldfire (added)

Comment:

 Aha.  What I see is
 {{{
 T9918.hs:64:32:
     Could not deduce (MonadRaise'
                         (TEQ (IORT s' m') (IORT s (IORT s' m')))
                         (IORT s' m')
                         (IORT s (IORT s' m')))
       arising from a use of ‘shPutStrLn’
     from the context (RMonadIO m')
       bound by the inferred type of
                test_copy :: RMonadIO m' => t -> FilePath -> IORT s' m' ()
       at T9918.hs:(60,1)-(64,49)
     In the second argument of ‘(>>=)’, namely ‘shPutStrLn hout’
     In the second argument of ‘till’, namely
       ‘(return "foo" >>= shPutStrLn hout)’
     In a stmt of a 'do' block:
       till (return True) (return "foo" >>= shPutStrLn hout)
 }}}
 You are wondering why the first argument to `MonadRaise'`, namely `(TEQ
 (IORT s' m') (IORT s (IORT s' m')))`, doesn't reduce to `False`.  Answer,
 because the first equation `TEQ m m` is not "surely apart" from `TEQ (IORT
 s' m') (IORT s (IORT s' m'))`.

 You may say that to make the first equation for `TEQ` succeed, we would
 need `m' = IORT s' m'`, which could only happen for infinite types.  But,
 as you'll see from [http://research.microsoft.com/en-
 us/um/people/simonpj/papers/ext-f/ our closed type-families paper], we
 found that we had to use a slightly more conservative check, one that
 allows infinite types, for the surely-apart check.

 Why doesn't the same thing happen for overlapping type-classes; here GHC
 does decide that the two type can't be equal (because of the occurs check)
 and so picks the second commented-out instance, for `MonadRaise m1 m2`.

 So there are some interesting things here
  * Your program depends in a very delicate way on the treatment of
 infinite types.  I wonder if it needs to?

  * Closed type families and type classes are treated differently.  That
 seems inconsistent.  In this particular example, I'm not sure which is
 "right".  I'm adding Richard to cc because he may have a view.

 Simon

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9918#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler