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

[GHC]

#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:  Unknown/Multiple  |            Architecture:
 Type of failure:  None/Unknown      |  Unknown/Multiple
      Blocked By:                    |               Test Case:
 Related Tickets:                    |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------

Comment (by oleg):

 I too have tried to induce unsoundness with overlapping instances and
 concluded it is unlikely -- although there is plenty of strange and
 incoherent behavior one can observe. The straightforward attempt to
 pack an existential in one type class environment and unpack it in
 another module (where a more specialized instance is introduced) does
 not work because the existential is packed with the corresponding
 dictionary. When it is unpacked, the packed dictionary is used --
 regardless how many new instances become available.

 Without type families, a type variable always stood for some ground
 type, at least potentially. When we assert a constraint C a on the
 type variable a, that constraint will not be dropped or discarded. It
 will be explicitly passed around, until it is resolved (or cannot be
 resolved -- in which case an error is reported). That is why it is
 safe to do instance selection for unground types: if we have
 {{{
 class C a where foo :: a -> Int
 instance C [a] where foo = length

 test3 x = foo [x]
 }}}
 the inferred type for test3 :: t -> Int has no constraints. We
 resolved C [t] for the unground type t. If t had other constraints,
 they will be preserved.

 With type functions, we are no longer sure what the type variable
 represents. It can be a non-reduced type-function application. So a
 type variable now stands not for a value (ground type) but for an
 expression. And that could be a problem. For example:
 {{{
 type family TT a
 -- no instances

 newtype D a = D{unD:: [TT a]}

 test4 (x::a) = foo (unD (undefined:: D a))

 test5 (x::a) = foo (unD (D []:: D a))
 }}}
 The code type-checks and test5 () even runs, returning 0. So,
 although T a has no instances, we have successfully ignored that fact.
 That trick would not have worked with only type classes; if we add a
 constraint we can't cast it away, and the type checker will demand
 sooner or later the constraint be satisfied.

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