Opened 2 years ago

Closed 17 months ago

#14442 closed bug (invalid)

InstanceSigs fails

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.3
Keywords: InstanceSigs Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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> 

Change History (3)

comment:1 Changed 2 years ago by simonpj

Suppose you'd written the instance decl like this

instance EQ Bool where
  eq = my_eq

my_eq :: Sing (x :: Bool) -> Sing (y :: Bool) -> Maybe (x :~~: y)
my_eq SFalse SFalse = Just HRefl

That works. Now remove the kind signature on x :: Bool. Fails. And indeed it should, because my_eq's signature means

my_eq :: forall k (x::k) (y::Bool). Sing x -> Sing (y :: Bool) -> Maybe (x :~~: y)

and indeed the code does not have this type.

So I think it's behaving right.

Can you suggest a concrete improvement to the user manual that would make that clearer?

comment:2 Changed 2 years ago by RyanGlScott

Status: newinfoneeded

Awaiting feedback from Iceland_jack.

comment:3 Changed 17 months ago by RyanGlScott

Resolution: invalid
Status: infoneededclosed

As mentioned in comment:1, this is not a bug.

Note: See TracTickets for help on using tickets.