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 |