Opened 4 years ago

Closed 3 years ago

Last modified 3 years ago

#11348 closed bug (fixed)

Local open type families instances ignored during type checking

Reported by: alexvieth Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.0.1-rc1
Keywords: TypeFamilies Cc: jstolarek
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T11348
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D1762
Wiki Page:

Description

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeInType #-}

import Data.Kind
import Data.Proxy

type family TrivialFamily t :: Type
type instance TrivialFamily (t :: Type) = Bool

data R where
    R :: Proxy Bool -> R

type ProblemType t = 'R ('Proxy :: Proxy (TrivialFamily t))

Compiling this program as-is, GHC rejects it!

error:
    • Expected kind ‘Proxy Bool’,
        but ‘'Proxy’ has kind ‘Proxy (TrivialFamily t)’
    • In the first argument of ‘R’, namely
        ‘(Proxy :: Proxy (TrivialFamily t))’
      In the type ‘R (Proxy :: Proxy (TrivialFamily t))’
      In the type declaration for ‘ProblemType’

But if we move TrivialFamily to another module and import it, GHC discovers that TrivialFamily t = Bool and the program is accepted.

When compiling the rejected program (with the local family instance) I observe that the instance environments given by FamInst.tcGetFamInstEnvs contain no instances! The renamer processes the local instance, but no FamInst is created for it, and nothing enters the TcGblEnv's family instance record.

Attachments (3)

0002-Fix-11348-collect-module-local-family-instances.patch (7.5 KB) - added by alexvieth 4 years ago.
A potential fix.
0002-Fix-11348-handle-instance-dependencies.patch (46.0 KB) - added by alexvieth 4 years ago.
Fix candidate 1
0002-Fix-11348-handle-instance-dependencies.2.patch (42.5 KB) - added by alexvieth 4 years ago.
Fix candidate 2

Download all attachments as: .zip

Change History (23)

Changed 4 years ago by alexvieth

A potential fix.

comment:1 Changed 4 years ago by alexvieth

Currently, we kind- and type-check TyClGroups before we even consider any family instances. I suppose this is ok without TypeInType, where the kind of a type cannot depend upon a family instance. But with it, seems we have to check our TyClGroups in tandem with our family instances! So the title of this ticket isn't so accurate; they're not ignored, they're just not considered until it's too late.

The patch is no good. I believe I now understand the problem and I'm working on another patch.

comment:2 Changed 4 years ago by goldfire

Yay yay yay. Thanks! The issue here is a known infelicity, but it seemed to me that fixing it would take a fair amount of reinstallation of plumbing. I think you'll have to type-check instance declarations (the first of the two passes in TcInstDcls) in with mutually recursive groups. A type whose kind mentions an open type family depends on the instances of that family.

If you're up to this task, that would be wonderful. I'm more than happy to advise.

comment:3 Changed 4 years ago by simonpj

Can someone explain the problem in more detail? Why should the instance declarations affect the kind of the type constructor?

Simon

comment:4 Changed 4 years ago by alexvieth

Why should the instance declarations affect the kind of the type constructor?

We could always find type families mentioned in GADT data constructors, but with GADT data constructor promotion, we can therefore find these families mentioned in kinds:

type family TrivialFamily (t :: Type) :: Type
type instance TrivialFamily t = Bool

data Q where
    Q :: TrivialFamily Int -> Q

-- The type of the data constructor
Q :: Bool -> Q

-- The kind of the promoted data constructor.
-- GHC actually gives 'Q :: TrivialFamily Int -> Q
-- but it *should* flatten that to Bool.
'Q :: Bool -> Q

-- This will not kind-check, unless we import the
-- TrivialFamily t instance.
type Problem = 'Q 'True

To check that a use of 'Q is well-kinded, we must know TrivialFamily Int. Pardon my earlier comment, this bug can arise without switching on TypeInType.

If you're up to this task, that would be wonderful.

Absolutely. This bug is blocking a project of mine so I want it fixed asap.

Changed 4 years ago by alexvieth

Fix candidate 1

comment:5 Changed 4 years ago by simonpj

You are so productive! But before generating a big patch, let's agree the design and approach.

Thanks for comment:4; I think I get it now. Here's another way to say it; see if you agree.

  • When kind-checking a type declaration, we must obviously first check the declarations of any types it mentions. E.g.
    type S = Int
    type T = S -> S
    
    We must kind-check S before T because T mentions S.
  • But we may also need to check a type instance declaration:
    type family F (a :: k) :: Type
    type instance F Int = Bool
    
    data K a = MK (F Int)
    type R = MK 'True
    
    In the declaration of R, the (promoted) data constructor MK is given an argument of kind Bool, but it expects one of kind F Int. Things only work if we have processed the type instance declaration first.
  • Alas, there is no explicit dependency of the declaration of R on the type instance declaration. Indeed we might also have
    type instance F R = ...blah...
    
    and we can't check that instance until after dealing with R.
  • Bottom line: we have to interleave processing of type/class decls with processing of type instance decls.

So I think the algorithm must be this: always process a type instance declaration as soon as all the type constructors it mentions have been kind-checked.

Algorithmically, we can't just add the type instance declarations to the strongly-connected component analysis for type/class decls, because of the lack of explicit dependencies. I think we have to

  • Do SCC on the type and class declarations as now
  • Keep in hand the set of un-processed type instance declarations
  • Before doing a type/class SCC, first process all the type instance decls whose free vars are imported, or are now bound in the type environment.
  • That results in a depleted set of un-processed type instance declarations.

Does that sound right? Is it what your patch does?

Incidentally this couldn't happen before TypeInType because previously we didn't promote data types like K.

Foo.hs:9:10:
    Data constructor ‘MK’ comes from an un-promotable type ‘K’
    In the type ‘MK True’

comment:6 Changed 4 years ago by alexvieth

So I think the algorithm must be this: always process a type instance declaration as soon as all the type constructors it mentions have been kind-checked.

Yes I believe this is the way forward. Your description of the problem is spot on, and the third bullet is particularly important.

With my patch, all InstDecls (even data and class instances) enter the dependency graph. Every InstDecl depends upon its class or family and the FreeVars determined by the renamer, while every TyClDecl which mentions a type family or class depends also upon every one of its instances known to the renamer. But given the third bullet point, this method is too coarse; type R = MK 'True should not depend upon type instance F R.

Algorithmically, we can't just add the type instance declarations to the strongly-connected component analysis for type/class decls, because of the lack of explicit dependencies.

As far as I can tell, there is enough information to add them, except when dealing with instances of imported families. Consider this example (from a note in the patch)

--A.hs
  type family Closed (t :: Type) :: Type where
      Closed t = Open t

  type family Open (t :: Type) :: Type
                                                                                
-- B.hs
  import A

  data Q where
      Q :: Closed Bool -> Q
                 
  type instance Open Int = Bool
                                                                                
  type S = 'Q 'True

We must ensure that type instance Open Int = Bool comes before type S = 'Q 'True, but 'Q doesn't depend directly upon Open, and we don't know that Closed depends upon Open! Although we add type instance Open Int to the dependency graph, we don't have enough information to connect it with type S, but this is OK so long as we fulfil the aforementioned goal:

always process a type instance declaration as soon as all the type constructors it mentions have been kind-checked.

In the patch, we achieve this by doing dependency analysis in two passes

  1. Add a new "meta-node" dependent upon every InstDecl, and on which every TyClDecl depends.
  2. Compute SCCs of this augmented graph.
  3. For every SCC, remove the meta-node and recompute the SCC.
  4. Concatenate these SCCs.

If an InstDecl does not depend upon a TyClDecl, then it will appear in an SCC of the augmented graph before the SCC in which the TyClDecl appears, thanks to the made-up dependency of the TyClDecl on every InstDecl.

I'm not sure I follow your description of the algorithm. The first bullet says we do SCC on the TyClDecls, but the third point says that before we do this, we must process the InstDecls. Did you mean that we keep SCC as is, with just TyClDecls, and during type-checking of the groups, we ensure that when an InstDecls dependencies are met, we check it immediately? That seems simpler and less invasive than my approach, and doesn't suffer from the problem shown by the third bullet. But it's not clear to me how to efficiently determine when an InstDecls dependencies have been met. We wouldn't want to scan the entire set each time we process a TyClDecl, no?

comment:7 Changed 4 years ago by simonpj

Yes, exactly. That is much simpler than "meta-nodes", and had the great merit of being correct (see third bullet).

I'm not too stressed about efficiency. You need only do this for the open type-family instances, and there are seldom zillions of them. If you want something a bit more efficient, try this:

  • Start with a set of pairs (fam-inst-decl, free-vars), where free-vars is a list of locally-defined type/class constructors mentioned anywhere in the instance. I'll call them the gate vars of the fam-inst-decl.
  • Typecheck any instances whose gate list is empty.
  • Turn the set of pairs into a finite map as follows: for each pair (fid, g:gs), add g -> (fid, gs) to the finite map. Tis is the gate map.
  • After typechecking a SCC of types/classes, take each one T in turn. Look up T in the gate map. For each (fid, gs) that it maps to, if gs is empty, that instance is ready to typecheck; if not, take one gate from gs. If it already in the type env, drop it and take another from gs. Once you find on active gate (i.e. not yet type-checked) and re-add the depleted pair to the gate map as before.

That's it really. Essentially we cross off the gate vars one by one until none are left.

You'd need to document this carefully.

comment:8 Changed 4 years ago by alexvieth

Yes, exactly. That is much simpler than "meta-nodes", and had the great merit of being correct (see third bullet).

Agreed. My graph approach was all wrong, so I've ditched it.

I think it would be ideal if we didn't have to plumb the FreeVars past rnSrcDecls and onto tcTyAndClassDecls, so I've come up with a solution which does essentially what you've described but during dependency analysis.

  1. Compute the SCCs for TyClDecls as we do now in HEAD.
  2. For all of the InstDecls (I includes class and data family instances. Any harm in doing so?), associate it with its FreeVars, intersected with the set of Names of TyClDecls that we just analysed.
  3. Fold the list of SCCs, at each step extracting the set of InstDecls for which its FreeVars is empty, and then eliminating all of the Names found in that SCC. That set of InstDecls, if non-empty, comes before the current component in the output list.

Will upload the patch in a few seconds.

Changed 4 years ago by alexvieth

Fix candidate 2

comment:9 Changed 4 years ago by jstolarek

alexvieth, could you upload your patches to Phab? This is our preferred method of uploading and reviewing patches. See also this wiki page: Phabricator.

comment:10 Changed 4 years ago by thomie

Status: newpatch

alexvieth: your patch is missing a test. See Building/RunningTests/Adding. Also, make sure your patch validates. Edit: the easiest way to do so is to submit it to Phabricator.

Last edited 4 years ago by thomie (previous) (diff)

comment:11 Changed 4 years ago by alexvieth

Diff created https://phabricator.haskell.org/D1762

A few tests fail due to a changeup in the order of type errors (since instance and tycl decl checking is interleaved). Will need some advice on what to do about that.

comment:12 Changed 4 years ago by thoughtpolice

Differential Rev(s): Phab:D1762

comment:13 Changed 4 years ago by jstolarek

Cc: jstolarek added

comment:14 Changed 4 years ago by thomie

Keywords: TypeFamilies added

comment:15 Changed 3 years ago by Simon Peyton Jones <simonpj@…>

In 353d8ae6/ghc:

SCC analysis for instances as well as types/classes

This big patch is in pursuit of Trac #11348.

It is largely the work of Alex Veith (thank you!), with some
follow-up simplification and refactoring from Simon PJ.

The main payload is described in RnSource
  Note [Dependency analysis of type, class, and instance decls]
which is pretty detailed.

* There is a new data type HsDecls.TyClGroup, for a strongly
  connected component of type/class/instance/role decls.

  The hs_instds field of HsGroup disappears, in consequence

  This forces some knock-on changes, including a minor
  haddock submodule update

Smaller, weakly-related things

* I found that both the renamer and typechecker were building an
  identical env for RoleAnnots, so I put common code for
  RoleAnnotEnv in RnEnv.

* I found that tcInstDecls1 had very clumsy error handling, so I
  put it together into TcInstDcls.doClsInstErrorChecks

comment:16 Changed 3 years ago by simonpj

Resolution: fixed
Status: patchclosed
Test Case: typecheck/should_compile/T11348

OK, done. Thank you to Alex Vieth for doing all the heavy lifting; the above patch is mostly his work.

Simon

comment:17 Changed 3 years ago by goldfire

Hooray Hooray Hooray! Thanks, Alex! This was a major engineering task that I shuddered at the thought of. It has lightened my day knowing that I won't have to do this. :)

If that was fun for you, the next step is to support induction recursion. I'm pretty sure I know how to do this, but it will take a similar engineering effort. It's not for the faint of heart, but this patch shows that your heart is not faint. As an added bonus, supporting induction recursion in GHC may be enough to publish a paper about, if that kind of thing is an incentive for you. Some notes (meant for myself, YMMV) I have on the subject are here.

comment:18 Changed 3 years ago by alexvieth

Happy to help! I'm glad to see this all wrapped up.

If that was fun for you, the next step is to support ​induction recursion.

Is there a trac ticket for this?

comment:19 Changed 3 years ago by goldfire

Yes, #11962.

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

In a4f2b76/ghc:

testsuite: Add regression test for #12381

Test Plan: Validate

Reviewers: austin

Subscribers: thomie

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

GHC Trac Issues: #12381, #11348
Note: See TracTickets for help on using tickets.