Unexpected behavior involving closed type families and repeat occurrences of variables
I'd expect both of these to work fine, but GHC always picks the instance that is mentioned first:
{-# LANGUAGE TypeFamilies, DataKinds #-}
type family Bad a b where
Bad (f a) a = False
Bad a a = True
bad :: ( Bad (f a) a ~ False
, Bad a a ~ True
) => ()
bad = ()
-- Swapping the lines around does not change the behavior much:
type family Bad' a b where
Bad' a a = True
Bad' (f a) a = False
bad' :: ( Bad' (f a) a ~ False
, Bad' a a ~ True
) => ()
bad' = ()
{-
ctf.hs:7:8:
Could not deduce (Bad a0 a0 ~ 'True)
from the context (Bad (f a) a ~ 'False, Bad a a ~ 'True)
bound by the type signature for
bad :: (Bad (f a) a ~ 'False, Bad a a ~ 'True) => ()
at ctf.hs:(7,8)-(9,14)
The type variable ‘a0’ is ambiguous
In the ambiguity check for:
forall (f :: * -> *) a.
(Bad (f a) a ~ 'False, Bad a a ~ 'True) =>
()
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘bad’:
bad :: (Bad (f a) a ~ False, Bad a a ~ True) => ()
ctf.hs:18:9:
Could not deduce (Bad' (f0 a0) a0 ~ 'False)
from the context (Bad' (f a) a ~ 'False, Bad' a a ~ 'True)
bound by the type signature for
bad' :: (Bad' (f a) a ~ 'False, Bad' a a ~ 'True) => ()
at ctf.hs:(18,9)-(20,14)
The type variables ‘f0’, ‘a0’ are ambiguous
In the ambiguity check for:
forall (f :: * -> *) a.
(Bad' (f a) a ~ 'False, Bad' a a ~ 'True) =>
()
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In the type signature for ‘bad'’:
bad' :: (Bad' (f a) a ~ False, Bad' a a ~ True) => ()
-}
Trying to turn this into an open type family instead somewhat hints at the issue:
type family Bad'' a b :: Bool
type instance Bad'' a a = True
type instance Bad'' (f a) a = False
{-
ctf.hs:58:15:
Conflicting family instance declarations:
Bad'' a a -- Defined at ctf.hs:58:15
Bad'' (f a) a -- Defined at ctf.hs:59:15
-}
It seems like GHC thinks these two family definitions conflict, yet to me they seem distinct - as a type that would match both would imply f a ~ a and hence be infinite.
Can anybody offer insight into this issue?
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |