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

Comment (by oleg):

 Perhaps the following two examples, deliberately simple, better illustrate
 the problem -- the difference in behavior of overlapping instances and
 closed type families.

 Example1:
 {{{
 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts
 #-}
 {-# LANGUAGE UndecidableInstances, OverlappingInstances #-}
 {-# LANGUAGE TypeFamilies #-}

 module Sub where

 data Z = Z
 data S n = S n

 -- x is greater than y by some amount
 class Sub x y where
   how_larger_is_x_than_y :: x -> y -> Int

 instance Sub x x where
   how_larger_is_x_than_y _ _ = 0

 instance (x ~ (S x1), Sub x1 y) => Sub x y where
   how_larger_is_x_than_y ~(S x) y = 1 + how_larger_is_x_than_y x y


 -- The inferred type shows no constraints! So we obtained the result
 -- without instantiating the type of y, hence maintaining polymorphism.

 test y = how_larger_is_x_than_y (S (S y)) y
 -- inferred type:
 --  test :: x1 -> Int

 main = test (S Z)
 -- 2
 }}}

 Example 2: rewritten using type families. This is how we hoped closed type
 families could eliminate overlapping instances.
 {{{
 {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts
 #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE ScopedTypeVariables #-}

 module Sub1 where

 data Z = Z
 data S n = S n

 class Nat a where
   nat :: a -> Int
 instance Nat Z where
   nat _ = 0
 instance Nat n => Nat (S n) where
   nat ~(S n) = 1 + nat n

 type family Sub x y :: * where
   Sub x x = Z
   Sub (S x) y = S (Sub x y)

 how_larger_is_x_than_y :: forall x y. (Nat (Sub x y)) => x -> y -> Int
 how_larger_is_x_than_y x y = nat (undefined :: Sub x y)

 -- The inferred type has the unresolved constraint

 test y = how_larger_is_x_than_y (S (S y)) y
 -- test :: Nat (Sub (S (S y)) y) => y -> Int

 main = test (S Z)
 -- 2
 }}}

 As you can see, with overlapping instances, GHC was able to eliminate the
 constraints on test. But with closed type families, it could not. There
 are no incoherent instances here, btw. In this simple example, the fact
 that test in the second example is no longer fully polymorphic does not
 matter. The code works anyway. But it does matter in the original
 (submitted) example.

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