Generalized injective type families
Needs RevisionPublic

Authored by jstolarek on Sep 28 2015, 4:20 AM.

Details

Summary

Generalization of injective type families to match the expressiveness of
functional dependencies, as briefly outlined in Section 7 of "Injective type
families for Haskell" Haskell Symposium 2015 paper. See also injectivity of
type C described on the wiki page
https://ghc.haskell.org/trac/ghc/wiki/InjectiveTypeFamilies

Test Plan

./validate

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Branch
T10832-generalized-injectivity
Lint
Lint WarningsExcuse: wontfix
SeverityLocationCodeMessage
Warninglibraries/template-haskell/Language/Haskell/TH/Lib.hs:44TXT3Line Too Long
Unit
No Unit Test Coverage
Build Status
Buildable 5835
Build 6445: GHC Patch Validation (amd64/Linux)
Build 6444: arc lint + arc unit
jstolarek updated this revision to Diff 4340.Sep 28 2015, 4:20 AM
jstolarek retitled this revision from to Generalized injective type families.
jstolarek updated this object.
jstolarek edited the test plan for this revision. (Show Details)
jstolarek added reviewers: simonpj, goldfire.
jstolarek updated the Trac tickets for this revision.
jstolarek planned changes to this revision.Sep 28 2015, 4:21 AM
jstolarek edited edge metadata.
jstolarek added a project: GHC.
jstolarek requested a review of this revision.Sep 28 2015, 7:10 AM

I've run into a problem and need help. Suppose I say:

type family F a = r | r -> a

Attempting to compile this declaration results in an error:

T10832.hs:4:23: error:
    GHC internal error: ‘r’ is not in scope during type checking, but it passed the renamer
    tcl_env of environment: [amg :-> Type variable ‘a’ = a,
                             r0 :-> AThing * -> *]
    In the type family declaration for ‘F’

This error is triggered in TcTyClsDecls.tcInjectivityCond:

tcInjectivityCond tvs (L loc (InjectivityCond lInjNames rInjNames))
  = setSrcSpan loc $
    do { inj_l_tvs <- mapM tcFdTyVar lInjNames -- HERE

But my guess is that the actual cause is elsewhere, namely in RnSource.rnFamDecl. There we bind type variables from type family head via call to bindHsTyVars BUT we do not bind the result type variable. Up till now this did not show up as a problem because we did not reference LHS of injectivity condition in the typechecker (see inline comments).

When working on injective type families we considered adding the result type variable to the list of type variables passed to bindHsTyVars in RnSource.rnFamDecl. But that didn't work because then TcTyClsDecls.tc_fam_ty_pats would report wrongNumberOfParmsErr.

There is one thing I don't understand here. We bind normal type variables by calling bindHsTyVars. Then we bind the result type variable by a call to bindLocalNames in RnSource.rnInjectivityCond. Normal type variables are correctly added to the environment, but the result variable is not. However bindHsTyVars ultimately calls bindLocalNames, so why the difference in behaviour?

compiler/typecheck/TcTyClsDecls.hs
796

Note that here LHS of injectivity annotation was ignored and so the problem did not show up.

803

But now we reference LHS of injectivity condition and so the problem manifests itself.

bgamari edited edge metadata.Nov 11 2015, 4:19 AM

@simonpj, do you think you could look at this when you get a chance?

bgamari added a comment.EditedDec 23 2015, 10:20 AM

@jstolarek, it appears that @simonpj committed a variant of this in rGHC332bc0d3af0a208ad310ce28cf798d4682423329. Perhaps you could mark this Diff as abandoned?

Oops, never mind. It was just committed to a branch.

bgamari requested changes to this revision.Jan 23 2016, 12:52 PM
bgamari edited edge metadata.

Bumping out of the review queue for now.

This revision now requires changes to proceed.Jan 23 2016, 12:52 PM
austin resigned from this revision.Nov 6 2017, 10:14 PM