[GHC] #9063: Default associated type instances are too general
#9063: Default associated type instances are too general ------------------------------------+------------------------------------- Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Keywords: | Operating System: Unknown/Multiple Architecture: Unknown/Multiple | Type of failure: None/Unknown Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | ------------------------------------+------------------------------------- I compile the following with `-ddump-tc` and `-fprint-explicit-kinds`: {{{ {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #-} module Bug where import Data.Type.Equality import Data.Proxy class kproxy ~ 'KProxy => PEq (kproxy :: KProxy a) where type (:==) (x :: a) (y :: a) :: Bool type x :== y = x == y }}} and I see {{{ TYPE SIGNATURES TYPE CONSTRUCTORS PEq :: forall (a :: BOX). KProxy a -> Constraint class (~) (KProxy a) kproxy (KProxy a) => PEq (a::BOX) (kproxy::KProxy a) Roles: [nominal, nominal] RecFlag NonRecursive type family (:==) (a::BOX) (x::a) (y::a) :: Bool (open) Defaults: [(k, BOX), (x, k), (y, k)] k x y = (==) k x y COERCION AXIOMS axiom Bug.NTCo:PEq :: PEq a kproxy = (~) (KProxy a) kproxy ('KProxy a) }}} The problem is the `Defaults:` line. That `k` should be an `a`. This is not a printing/tidying problem -- the default does not work when it should. For example, if I add the following {{{ instance PEq ('KProxy :: KProxy Bool) foo :: Proxy (True :== True) -> Proxy (True == True) foo = id }}} I get {{{ Couldn't match type ‘(:==) Bool 'True 'True’ with ‘'True’ Expected type: Proxy Bool ((:==) Bool 'True 'True) -> Proxy Bool ((==) Bool 'True 'True) Actual type: Proxy Bool 'True -> Proxy Bool 'True In the expression: id In an equation for ‘foo’: foo = id }}} Adding kind signatures (that is `:: a`) to the arguments of the type family default fixes the problem. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): This problem also exists for instances, possibly leading to spurious overlapping instance errors. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by simonpj): Can you give an example for instances? There is a design question here. For a start, the associated type should really mention at least one of the class variables. This should be prohibited: {{{ class C a where type F b :: * }}} Second, the default instances should mention the same class variable in the same position, not some pattern. For example {{{ class C a where type F a b :: * type instance F a Int = Int -- OK type instance F a Bool = Char -- OK type instance F Int a = Bool -- Definitely not OK! type instance F [a] b = Char -- Not OK }}} Reason: the default instances are simply templates, from which you can create the real `type instance` in the instance decl. For example {{{ instance C Float -- type instance F Float Int = Int -- type instance F Float Bool = Char }}} How would one instantiate the "not-ok" defaults here?? We are not currently checking any of this, nor is it documented. [http://www.haskell.org/ghc/docs/7.8.2/html/users_guide/type-families.html #assoc-decl-defs Current manual entry] Before moving to fix it, let's just check that we agree. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): Here is an example where this problem bites in instances: {{{ {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators #-} module Bug where import Data.Proxy class kproxy ~ 'KProxy => PEq (kproxy :: KProxy a) where type (:==) (x :: a) (y :: a) :: Bool instance PEq ('KProxy :: KProxy Bool) where type False :== False = True type False :== True = False type True :== False = False type True :== True = True instance PEq ('KProxy :: KProxy ()) where type x :== y = True }}} I get {{{ Type indexes must match class instance head Found ‘k’ but expected ‘()’ In the type instance declaration for ‘:==’ In the instance declaration for ‘PEq (KProxy :: KProxy ())’ }}} That's not an overlapping instance error -- I was wrong in my post above. I guess I didn't look closely at the error. But, GHC should be able to figure out what I mean here. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): I agree with most of Simon's analysis. The "not OK" instances are definitely not OK, and should be rejected. But, my case is subtly different, in that I'm not asking for magic, just kind-checking. What makes my case different is that the class parameter is a kind variable. Here is how I want GHC to reason, in the example in my original report: - The type family declaration introduces the identifier `(:==)`, with kind `a -> a -> Bool`, where `a` is the class (kind) variable. - When kind-checking the default instance, we kind-check with expected kind `a` for `x` and expected kind `a` for `y`. - The kind-checked, desugared LHS of the default instance indeed does mention a class variable `a`, in exactly the right spot. - Definition accepted. In the instance case, a similar analysis works out: we kind-check the instance for `(:==)` using the instantiated kind (`() -> () -> Bool` in the second instance in my comment above), and everything works out. I ''do'' see the counterargument here, that it seems I'm asking for magic. But, I respectfully disagree with that stance. And, it would seem that the implementation here would be rather straightforward and I'm happy to do it. Regardless of the outcome, we should probably flesh out that manual entry. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): It might help to note ''why'' I'm pushing this. I'm working on expanding the promotion algorithm in the `singletons` package to include classes and instances. I want to promote method definitions to associated type family instances. Currently, something like this is peachy: {{{ instance Eq () where _ == _ = True }}} However, with the current treatment of associated type instances as discussed here, the promoted version of this (in my "instance example" above) does not work without explicit kind annotations. My implementation currently has to store method types, do a lookup on method definitions, and then do a type substitution to produce the needed kind annotations. This isn't terribly hard, really, but it just seems unnecessary. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general
-------------------------------------+------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Simon Peyton Jones
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Comment (by goldfire): This might just be related to #9151. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general -------------------------------------+------------------------------------ Reporter: goldfire | Owner: simonpj Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: Unknown/Multiple Type of failure: None/Unknown | Difficulty: Unknown Test Case: | Blocked By: Blocking: | Related Tickets: -------------------------------------+------------------------------------ Changes (by simonpj): * owner: => simonpj Comment: I have a fix for this done, but not yet pushed. It'll have to wait till I get back from holiday. Simon -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#9063: Default associated type instances are too general
-------------------------------------+------------------------------------
Reporter: goldfire | Owner: simonpj
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture: Unknown/Multiple
Type of failure: None/Unknown | Difficulty: Unknown
Test Case: | Blocked By:
Blocking: | Related Tickets:
-------------------------------------+------------------------------------
Comment (by Simon Peyton Jones
#9063: Default associated type instances are too general -------------------------------------+------------------------------------- Reporter: goldfire | Owner: simonpj Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 7.8.2 Resolution: fixed | Keywords: Differential Revisions: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: polykinds/T9063 Difficulty: Unknown | Blocking: Blocked By: | Related Tickets: | -------------------------------------+------------------------------------- Changes (by simonpj): * status: new => closed * testcase: => polykinds/T9063 * resolution: => fixed -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/9063#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC