#14442: InstanceSigs fails -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.3 Keywords: InstanceSigs | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- 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: {{{#!hs {-# 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> }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14442 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler