[GHC] #9063: Default associated type instances are too general

2 May 2014

      #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