It seems to me that GHC should be able to ''conclude'' from `f x ~ g y`
#9725: Constraint deduction failure -------------------------------------+------------------------------------- Reporter: heisenbug | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: Resolution: | Architecture: Unknown/Multiple Operating System: | Difficulty: Unknown Unknown/Multiple | Blocked By: Type of failure: GHC | Related Tickets: rejects valid program | Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:1 rwbarton]: that `f` and `g` have the same kind, but maybe it has no way to represent this?
I think there is a related Trac ticket also, but I couldn't find it.
Maybe adding kind annotations for some of the type variables involved
would help? I don't know what you're doing, but if I understand what you're getting at, I don't think it's true in general. Consider {{{#!hs {-# LANGUAGE TypeFamilies, TypeOperators, KindSignatures #-} module ConstraintEq where type family Id a :: * where Id x = x type family YaKnow a :: * where YaKnow x = x Int }}} Here `Id Int ~ YaKnow Id`, but `Id` and `YaKnow` have different kinds. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9725#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler