Inconsistent type family resolution

This is as small as I'm able to make the example. It uses the 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.

{-# 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 this StackOverflow post.

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture