InstanceSigs fails
This may be expected behavior, resulting from instance signatures being allowed to be "more polymorphic" than the method @Bool
. But better safe than sorry (can't think of a better title).
This works fine:
{-# Language KindSignatures, GADTs, DataKinds, TypeOperators, PolyKinds, TypeFamilies, TypeFamilyDependencies, InstanceSigs #-}
import Data.Kind
import Data.Type.Equality
type family Sing = (res :: k -> Type) | res -> k
type instance Sing = SBool
data SBool :: Bool -> Type where
SFalse :: SBool False
STrue :: SBool True
class EQ a where
eq :: Sing (x::a) -> Sing (y::a) -> Maybe (x :~~: y)
instance EQ Bool where
eq :: Sing (x :: Bool) -> Sing (y :: Bool) -> Maybe (x :~~: y)
eq SFalse SFalse = Just HRefl
Removing the kind annotation from x :: Bool
and/or y :: Bool
causes it to fail: Here I have removed it from x
: eq :: Sing x -> Sing (y :: Bool) -> Maybe (x :~~: y)
$ ghci -ignore-dot-ghci B.hs
GHCi, version 8.3.20170920: http://www.haskell.org/ghc/ :? for help
[1 of 1] Compiling Main ( B.hs, interpreted )
B.hs:19:6: error:
• Couldn't match type ‘SBool’ with ‘Sing’
Expected type: Sing x
Actual type: SBool a0
• In the pattern: SFalse
In an equation for ‘eq’: eq SFalse SFalse = Just HRefl
In the instance declaration for ‘EQ Bool’
• Relevant bindings include
eq :: Sing x -> Sing y -> Maybe (x :~~: y) (bound at B.hs:19:3)
|
19 | eq SFalse SFalse = Just HRefl
| ^^^^^^
B.hs:19:22: error:
• Could not deduce: (x :: k1) ~~ ('False :: Bool)
from the context: a0 ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in an equation for ‘eq’
at B.hs:19:6-11
or from: y ~ 'False
bound by a pattern with constructor: SFalse :: SBool 'False,
in an equation for ‘eq’
at B.hs:19:13-18
‘x’ is a rigid type variable bound by
the type signature for:
eq :: forall k1 (x :: k1) (y :: Bool).
Sing x -> Sing y -> Maybe (x :~~: y)
at B.hs:18:9-54
Expected type: Maybe (x :~~: y)
Actual type: Maybe (x :~~: x)
• In the expression: Just HRefl
In an equation for ‘eq’: eq SFalse SFalse = Just HRefl
In the instance declaration for ‘EQ Bool’
• Relevant bindings include
eq :: Sing x -> Sing y -> Maybe (x :~~: y) (bound at B.hs:19:3)
|
19 | eq SFalse SFalse = Just HRefl
| ^^^^^^^^^^
Failed, 0 modules loaded.
Prelude>
Trac metadata
Trac field | Value |
---|---|
Version | 8.3 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |