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