Default associated type instances are too general
I compile the following with -ddump-tc
and -fprint-explicit-kinds
:
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators,
UndecidableInstances #-}
module Bug where
import Data.Type.Equality
import Data.Proxy
class kproxy ~ 'KProxy => PEq (kproxy :: KProxy a) where
type (:==) (x :: a) (y :: a) :: Bool
type x :== y = x == y
and I see
TYPE SIGNATURES
TYPE CONSTRUCTORS
PEq :: forall (a :: BOX). KProxy a -> Constraint
class (~) (KProxy a) kproxy (KProxy a) => PEq (a::BOX)
(kproxy::KProxy a)
Roles: [nominal, nominal]
RecFlag NonRecursive
type family (:==) (a::BOX) (x::a) (y::a) :: Bool (open)
Defaults: [(k, BOX), (x, k), (y, k)] k x y = (==) k x y
COERCION AXIOMS
axiom Bug.NTCo:PEq ::
PEq a kproxy = (~) (KProxy a) kproxy ('KProxy a)
The problem is the Defaults:
line. That k
should be an a
. This is not a printing/tidying problem -- the default does not work when it should. For example, if I add the following
instance PEq ('KProxy :: KProxy Bool)
foo :: Proxy (True :== True) -> Proxy (True == True)
foo = id
I get
Couldn't match type ‘(:==) Bool 'True 'True’ with ‘'True’
Expected type: Proxy Bool ((:==) Bool 'True 'True)
-> Proxy Bool ((==) Bool 'True 'True)
Actual type: Proxy Bool 'True -> Proxy Bool 'True
In the expression: id
In an equation for ‘foo’: foo = id
Adding kind signatures (that is :: a
) to the arguments of the type family default fixes the problem.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |