Opened 3 years ago

Closed 3 years ago

Last modified 2 years ago

#11837 closed bug (fixed)

GHC fails to unify kinds when deriving polykinded typeclass instance for polykinded newtype

Reported by: RyanGlScott Owned by: RyanGlScott
Priority: normal Milestone: 8.0.2
Component: Compiler (Type checker) Version: 8.0.1
Keywords: deriving Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #8865, #11833 Differential Rev(s): Phab:D2117
Wiki Page:

Description

This is failing:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE PolyKinds #-}
module Example where

class Category (cat :: k -> k -> *) where
  catId   :: cat a a
  catComp :: cat b c -> cat a b -> cat a c

newtype T (c :: k -> k -> *) a b = MkT (c a b) deriving Category

with the following error:

$ /opt/ghc/8.0.1/bin/ghc Example.hs -fprint-explicit-kinds -ddump-deriv
[1 of 1] Compiling Example          ( Example.hs, Example.o )

==================== Derived instances ====================
Derived instances:
  instance forall k_ayw k_ayx (c_ayy :: k_ayx
                                        -> k_ayx -> GHC.Types.*).
           Example.Category k_ayw c_ayy =>
           Example.Category k_ayw (Example.T k_ayx c_ayy) where
    Example.catId
      = GHC.Prim.coerce (Example.catId :: c_apb a_apg a_apg) ::
          forall (a_apg :: k_XxC). Example.T c_apb a_apg a_apg
    Example.catComp
      = GHC.Prim.coerce
          (Example.catComp ::
             c_apb b_aph c_api -> c_apb a_apj b_aph -> c_apb a_apj c_api) ::
          forall (b_aph :: k_XxC) (c_api :: k_XxC) (a_apj :: k_XxC).
          Example.T c_apb b_aph c_api
          -> Example.T c_apb a_apj b_aph -> Example.T c_apb a_apj c_api
  

GHC.Generics representation types:



Example.hs:9:57: error:
    • Expected kind ‘k1’, but ‘a1’ has kind ‘k’
    • In the second argument of ‘T’, namely ‘a’
      In an expression type signature: forall (a :: k). T c a a
      In the expression:
          GHC.Prim.coerce (catId :: c a a) :: forall (a :: k). T c a a
      When typechecking the code for ‘catId’
        in a derived instance for ‘Category k (T k c)’:
        To see the code I am typechecking, use -ddump-deriv
    • Relevant bindings include
        catId :: T k1 c a a (bound at Example.hs:9:57)

This is very similar to #11833, but in this scenario, both the datatype and typeclass are poly-kinded, and I believe the issue here is fundamentally different.

With -fprint-explicit-kinds, it becomes apparent what the issue is: for some reason, the kind variable of Category (k_ayw) is not unifying with the kind variable of T (k_ayx), resulting in a kind mismatch.

I'll fix this - patch incoming.

Change History (5)

comment:1 Changed 3 years ago by RyanGlScott

Differential Rev(s): Phab:D2117
Status: newpatch

comment:2 Changed 3 years ago by Ben Gamari <ben@…>

In e53f2180/ghc:

Fix deriveTyData's kind unification when two kind variables are unified

When `deriveTyData` attempts to unify two kind variables (which can
happen if both the typeclass and the datatype are poly-kinded), it
mistakenly adds an extra mapping to its substitution which causes the
unification to fail when applying the substitution. This can be
prevented by checking both the domain and the range of the original
substitution to see which kind variables shouldn't be put into the
domain of the substitution. A more in-depth explanation is included in
`Note [Unification of two kind variables in deriving]`.

Fixes #11837.

Test Plan: ./validate

Reviewers: simonpj, hvr, goldfire, niteria, austin, bgamari

Reviewed By: bgamari

Subscribers: niteria, thomie

Differential Revision: https://phabricator.haskell.org/D2117

GHC Trac Issues: #11837

comment:3 Changed 3 years ago by bgamari

Milestone: 8.0.2
Status: patchmerge

comment:4 Changed 3 years ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:5 Changed 2 years ago by RyanGlScott

Keywords: deriving added
Note: See TracTickets for help on using tickets.