[GHC] #9888: Inconsistent type family resolution

[GHC]

#9888: Inconsistent type family resolution
-------------------------------------+-------------------------------------
       Reporter:  crockeea           |                   Owner:
           Type:  bug                |                  Status:  new
       Priority:  normal             |               Milestone:
      Component:  Compiler           |                 Version:  7.8.3
       Keywords:                     |        Operating System:
   Architecture:  Unknown/Multiple   |  Unknown/Multiple
     Difficulty:  Unknown            |         Type of failure:  GHC
     Blocked By:                     |  rejects valid program
Related Tickets:                     |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:
-------------------------------------+-------------------------------------
 This is as small as I'm able to make the example. It uses the
 [http://hackage.haskell.org/package/singletons singletons] library. If I
 write my own `Map` type family, I can get the code to work. However, there
 seems to be a problem in GHC since I get seemingly conflicting information
 in GHCi.

 {{{#!hs
 {-# LANGUAGE TypeFamilies, TypeOperators, DataKinds,
              FlexibleContexts, UndecidableInstances #-}

 module Foo where

 import Data.Singletons.Prelude hiding (And)

 -- if every type in the list is equal, `CommonElt` returns the common type
 type family CommonElt xs where
   CommonElt (x ': xs) =
     EqResult (And (Map ((TyCon2 (==)) $ x) xs)) x

 type family a == b where
   a == a = 'True
   a == b = 'False

 type family And xs where
   And '[] = 'True
   And ('False ': xs) = 'False
   And ('True ': xs) = And xs

 -- converts a True result to a type
 type family EqResult b v where
   EqResult 'True r = r

 type R = CommonElt '[Int, Int]

 f :: R
 f = 3
 }}}

 This code does not compile:

 {{{
 Foo.hs:30:5:
     No instance for (Num (EqResult (And ((Int == Int) :$$$ '[])) Int))
       arising from the literal ‘3’
     In the expression: 3
     In an equation for ‘f’: f = 3
 Failed, modules loaded: none.
 }}}

 But if I comment out `f` and load the rest of the file in GHCi, I can
 easily see that `R ~ Int`:

 {{{
 > :kind! R
 R :: *
 = Int
 }}}

 This seems suspicious to me because GHCi can resolve the type of `R`, but
 when code requiring `R` to be resolved is compiled (in GHCi or with GHC),
 I get the error above. I believe that `:kind!` is correctly resolving the
 type to `Int`, and that the type error is a bug.

 This is documented in more detail at
 [http://stackoverflow.com/questions/27490352/type-family-shenanigans-in-
 ghci this StackOverflow post].

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