Opened 11 months ago

Closed 5 months ago

#9151 closed bug (fixed)

Recursive default associated types don't kind-generalize properly

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.2
Keywords: Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: typecheck/should_compile/T9151
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

When I say

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies, UndecidableInstances #-}

module Bug where

import Data.Proxy

class PEnum (kproxy :: KProxy a) where
  type ToEnum (x :: a) :: Bool
  type ToEnum x = TEHelper

type TEHelper = ToEnum Int

I get

/Users/rae/temp/Bug.hs:11:24:
    The first argument of ‘ToEnum’ should have kind ‘a’,
      but ‘Int’ has kind ‘*’
    In the type ‘ToEnum Int’
    In the type declaration for ‘TEHelper’

I believe my original code should kind-check, as ToEnum should be applicable to any kind.

My guess is that this sort of recursion isn't properly accounted for in the kind-checking algorithm in TcTyClsDecls, and that we kind-check TEHelper before ToEnum is kind-generalized.

Change History (16)

comment:1 Changed 11 months ago by archblob

I have played with the test case a little to see if I can reduce it, and to see when exactly the error happens.

Here is what I have:

{-# LANGUAGE PolyKinds, TypeFamilies, UndecidableInstances #-}

module Bug where

class PEnum (k :: a) where
  type ToEnum (x :: a) :: *
  type ToEnum x = TEHelper

type TEHelper = ToEnum Int

That fails as the test case in the ticket, and this one passes:

{-# LANGUAGE PolyKinds, TypeFamilies, UndecidableInstances #-}

module Bug where

class PEnum (k :: a) where
  type ToEnum (x :: b) :: *
  type ToEnum x = TEHelper

type TEHelper = ToEnum Int

Also this is the output from -ddump-tc-trace :

rn12
rn13
Tc2 (src)
Tc3
kcTyClGroup
  module Bug
  class PEnum (k :: a) where
    type family ToEnum (x :: a) :: *
    type instance ToEnum x = TEHelper
  type TEHelper = ToEnum Int
env2 [(a, Type variable ‘a’ = a)]
env2 []
kcTyClGroup: initial kinds
  [(PEnum, AThing a -> Constraint), (ToEnum, AThing a -> *)]
env2 []
kcd1 TEHelper []
tc_lhs_type:
  ToEnum Int
  Expected kind ‘k_av5’
tc_lhs_type:
  ToEnum
  Expected kind ‘k_av6’
lk1 ToEnum
lk2 ToEnum AThing a -> *
writeMetaTyVar k_av6 := a -> *
tc_lhs_type:
  Int
  The first argument of ‘ToEnum’ should have kind ‘a’
lk1 Int
lk2 Int Type constructor ‘Int’
checkExpectedKind
  Int
  *
  a
checkExpectedKind 1
  Int
  *
  a
  ([(k0, 1)], [(av4, a)])
  ([(k0, 1)], [(av4, a)])
Adding error:
  Bug.hs:9:24:
      The first argument of ‘ToEnum’ should have kind ‘a’,
        but ‘Int’ has kind ‘*’
      In the type ‘ToEnum Int’
      In the type declaration for ‘TEHelper’
tryTc/recoverM recovering from IOEnv failure

Bug.hs:9:24:
    The first argument of ‘ToEnum’ should have kind ‘a’,
      but ‘Int’ has kind ‘*’
    In the type ‘ToEnum Int’
    In the type declaration for ‘TEHelper’

comment:2 Changed 11 months ago by goldfire

That second example is somewhat alarming -- the associated type family does not mention any class parameters. I'm surprised that's accepted!

comment:3 Changed 11 months ago by archblob

It really is.
Also, by playing with the kind checking strategy when default instances are defined I've managed to get the initial program to typecheck and get the correct type and kinds.

Last edited 11 months ago by archblob (previous) (diff)

comment:4 follow-up: Changed 11 months ago by archblob

That second example is somewhat alarming -- the associated type family does not mention > any class parameters. I'm surprised that's accepted!

@goldfire, wasn't this introduced in #7939 ?

comment:5 Changed 11 months ago by goldfire

Created #9167 about the malformed associated type issue.

@archblob: Do you have a patch about the original issue? Thanks for looking into it!

comment:6 in reply to: ↑ 4 Changed 11 months ago by goldfire

Replying to archblob:

That second example is somewhat alarming -- the associated type family does not mention > any class parameters. I'm surprised that's accepted!

@goldfire, wasn't this introduced in #7939 ?

Perhaps, but if so, it was certainly not intentional. That work should make b poly-kinded, but it shouldn't necessarily make F accepted. I'm actually surprised that kind-checking strategies have much to do with this bug, but I haven't looked into it. When you change strategies, how does that affect other programs? As outlined in the very long comment explaining them and in #7939, kind-checking strategies are fiddly and subtle, a dangerous combination.

comment:7 Changed 11 months ago by archblob

The patch for the original issue still needs validating, I'm working on it now. I was interested in tracking down when the other problem happened first.

comment:8 Changed 11 months ago by archblob

Although my patch fixed this specific problem, it failed validation by causing others.
My initial idea was to infer a more general forall (a :: BOX). a -> * kind when the associated type is mentioned in the rhs of the synonym, works for this case but causes breakages. Anyway, I'll be looking more into how to do it because I'm having a good time, but I'm not really sure anything will come of it so if someone else wants to work on this, don't mind me, go ahead.

comment:9 Changed 11 months ago by goldfire

Looking at the code for a bit, I don't think this is a trivial fix, after all. The problem is that associated type defaults are type-checked in the same group as the enclosing class. This means that GHC thinks that TEHelper and PEnum are mutually recursive. Thus, polymorphic recursion is not allowed between them, which is what we're asking for here.

Instead, GHC should type check associated type defaults with other instances (in tcInstDecls1, likely), after all TyClGroups are done being checked. With that line-up, TEHelper depends on ToEnum (part of the group with PEnum), but not the other way around. Unfortunately, this requires some moving plumbing around, and is not something I have time for at the moment. This all is not unlike how default method declarations have to be checked quite separately from the rest of a class.

Anyway, archblob, if you want to keep playing, perhaps my comments above are helpful. I don't think this is hard, but I originally thought the problem was due to a small oversight in the dependency analysis in the renamer. That's not the case, but it shouldn't be more than an hour or two of work.

comment:10 Changed 11 months ago by archblob

I think you original assumption still stands, as the current failure happens when we try to type-check the type synonym, we don't even get to the associated defaults, thus only postponing the type checking of atdefs will do no good I think. The failure will still happen at this stage. I think the synonym would have to be type checked in a different group, after the class declaration and before the atdefs, which will have to be checked with other instances as you suggested. Maybe someone else can chime in with some ideas about the strategy. Please tell me if my assumptions are wrong.

comment:11 Changed 11 months ago by archblob

  • Cc simonpj added

I'm adding simonpj, maybe he can chime in.

I'm writing again as documentation.
I've been looking into the result of the dependency analysis done in depAnalTyClDecls
and we have :

  REC
    type TEHelper = ToEnum Int

    class PEnum (k :: a) where
      type family ToEnum (x :: a) :: *
      type instance ToEnum x = TEHelper

which means we will try to check TEHelper before we generalize ToEnum and hence the kind check error.

Braking the cycle and having:

  REC
    class PEnum (k :: a) where
      type family ToEnum (x :: a) :: *
      type instance ToEnum x = TEHelper
  
  NOREC
    type TEHelper = ToEnum Int

will only work if we defer default type instance checking as you suggested. These modifications have to go together. But they really fell hackish.

One other thing that I don't know if we can do is somehow accommodate for this by tweaking the four steps in kcTyClGroup , I'll be looking into how to do that as an alternative and compare the two.

Am I making sense ?

comment:12 Changed 11 months ago by simonpj

archblob, you are digging into one of the darkest corners of the type inference engine. I don't have time to page all this in right now. My suggestion would be to tackle something easier for now.

Simon

comment:13 Changed 9 months ago by simonpj

I'm reluctant to change the way that associated type defaults are kind-checked; but solving #9200 will also allow this program to be kind-checked. ToEnum will be treated as having a CUSK, and hence will support polymorphic recursion.

Simon

comment:14 Changed 5 months ago by goldfire

Confirmed that the original program is accepted in HEAD. Adding a test case soon.

comment:15 Changed 5 months ago by Richard Eisenberg <eir@…>

In 67abfdacf5c93cccb0ab780b524591c916b21c3f/ghc:

Test #9151 in typecheck/should_compile/T9151.

This test case should pass right now -- the bug is fixed,
presumably by #9200.

comment:16 Changed 5 months ago by goldfire

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to typecheck/should_compile/T9151
Note: See TracTickets for help on using tickets.