[GHC] #15591: Inconsistent kind variable binder visibility between associated and non-associated type families
GHC
ghc-devs at haskell.org
Sat Sep 1 15:36:10 UTC 2018
#15591: Inconsistent kind variable binder visibility between associated and non-
associated type families
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner: (none)
Type: bug | Status: new
Priority: normal | Milestone: 8.6.1
Component: Compiler | Version: 8.5
Resolution: | Keywords:
| TypeApplications, TypeFamilies
Operating System: Unknown/Multiple | Architecture:
| Unknown/Multiple
Type of failure: None/Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Rev(s):
Wiki Page: |
-------------------------------------+-------------------------------------
Comment (by RyanGlScott):
I have somewhat of an idea why this is happening. The
[http://git.haskell.org/ghc.git/blob/565ef4cc036905f9f9801c1e775236bb007b026c:/compiler/rename/RnTypes.hs#l811
bindHsQTyVars] function appears to be partly to blame for this
discrepancy. `bindHsQTyVars` (which works over type families, among other
things) computes kind variables like so:
{{{#!hs
implicit_kvs = filter_occs rdr_env bndrs kv_occs
}}}
Where `filter_occs` is defined as:
{{{#!hs
filter_occs :: LocalRdrEnv -- In scope
-> [Located RdrName] -- Bound here
-> [Located RdrName] -- Potential implicit binders
-> [Located RdrName] -- Final implicit binders
-- Filter out any potential implicit binders that are either
-- already in scope, or are explicitly bound here
filter_occs rdr_env bndrs occs
= filterOut is_in_scope occs
where
is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env occ)
|| locc `elemRdr` bndrs
}}}
Note that this filters out any type variable names which appear in
`rdr_env`. This environment contains all type variables that have already
been bound, which includes any variables that were bound by the class
head. Therefore, in our original example, the `a` in `class C (a :: Type)`
ends up being filtered out entirely, so by the time we get to
typechecking, GHC thinks that `a` is an invisible argument.
One idea I had to fix this was to have `filter_occs` also return the
class-bound variables so that they could be put at the front of the other
kind variables. In other words, this patch:
{{{#!diff
diff --git a/compiler/rename/RnTypes.hs b/compiler/rename/RnTypes.hs
index a78caaf..2163495 100644
--- a/compiler/rename/RnTypes.hs
+++ b/compiler/rename/RnTypes.hs
@@ -841,7 +841,7 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs
hsq_bndrs thing_inside
-- Make sure to list the binder kvs
before the
-- body kvs, as mandated by
-- Note [Ordering of implicit variables]
- implicit_kvs = filter_occs rdr_env bndrs kv_occs
+ (cls_bound_nms, implicit_kvs) = filter_occs rdr_env bndrs
kv_occs
-- Deleting bndrs: See Note [Kind-
variable ordering]
-- dep_bndrs is the subset of bndrs that are dependent
-- i.e. appear in bndr/body_kv_occs
@@ -858,13 +858,14 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs
hsq_bndrs thing_inside
]
; implicit_kv_nms <- mapM (newTyVarNameRn mb_assoc) implicit_kvs
+ ; let all_implicit_nms = cls_bound_nms ++ implicit_kv_nms
; bindLocalNamesFV implicit_kv_nms $
bindLHsTyVarBndrs doc mb_in_doc mb_assoc hs_tv_bndrs $ \
rn_bndrs ->
do { traceRn "bindHsQTyVars" (ppr hsq_bndrs $$ ppr implicit_kv_nms $$
ppr rn_bndrs)
; dep_bndr_nms <- mapM (lookupLocalOccRn . unLoc) dep_bndrs
; thing_inside (HsQTvs { hsq_ext = HsQTvsRn
- { hsq_implicit = implicit_kv_nms
+ { hsq_implicit = all_implicit_nms
, hsq_dependent = mkNameSet
dep_bndr_nms }
, hsq_explicit = rn_bndrs })
all_bound_on_lhs } }
@@ -873,14 +874,25 @@ bindHsQTyVars doc mb_in_doc mb_assoc body_kv_occs
hsq_bndrs thing_inside
filter_occs :: LocalRdrEnv -- In scope
-> [Located RdrName] -- Bound here
-> [Located RdrName] -- Potential implicit binders
- -> [Located RdrName] -- Final implicit binders
+ -> ([Name], [Located RdrName])
+ -- (Class binders, final implicit binders)
-- Filter out any potential implicit binders that are either
-- already in scope, or are explicitly bound here
filter_occs rdr_env bndrs occs
- = filterOut is_in_scope occs
+ = partitionWith is_class_bound $
+ filterOut is_implicit occs
where
- is_in_scope locc@(L _ occ) = isJust (lookupLocalRdrEnv rdr_env
occ)
- || locc `elemRdr` bndrs
+ is_class_bound :: Located RdrName
+ -> Either Name (Located RdrName)
+ -- Left: a class-bound name
+ -- Right: bound by the type family itself
+ is_class_bound locc@(L _ occ) =
+ case lookupLocalRdrEnv rdr_env occ of
+ Just n -> Left n
+ Nothing -> Right locc
+
+ is_implicit :: Located RdrName -> Bool
+ is_implicit locc = locc `elemRdr` bndrs
{- Note [bindHsQTyVars examples]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
}}}
That fixes the original program, encouragingly enough:
{{{
$ inplace/bin/ghc-stage2 --interactive ../Foo.hs -fprint-explicit-foralls
GHCi, version 8.7.20180831: http://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Foo ( ../Foo.hs, interpreted )
Ok, one module loaded.
λ> :kind T2
T2 :: forall a (f :: * -> *). f a -> *
}}}
However, there's a catch. This causes a single test from the test suite to
fail: `T14131`.
{{{
=====> T14131(normal) 1 of 1 [0, 0, 0]
cd "indexed-types/should_compile/T14131.run" &&
"/home/rgscott/Software/ghc2/inplace/test spaces/ghc-stage2" -c
T14131.hs -dcore-lint -dcmm-lint -no-user-package-db -rtsopts -fno-warn-
missed-specialisations -fshow-warning-groups -fdiagnostics-color=never
-fno-diagnostics-show-caret -dno-debug-output
Compile failed (exit code 1) errors were:
T14131.hs:29:3: error:
• Type indexes must match class instance head
Expected: ZT
Actual: ZT
Use -fprint-explicit-kinds to see the kind arguments
• In the class declaration for ‘Z’
*** unexpected failure for T14131(normal)
}}}
For reference, here's the full definition of `ZT`:
{{{#!hs
class Z k where
type ZT :: Maybe k
type ZT = (Nothing :: Maybe k)
}}}
If you do use `-fprint-explicit-kinds`, the results aren't much more
informative:
{{{
[1 of 1] Compiling T14131 ( tests/indexed-
types/should_compile/T14131.hs, interpreted )
tests/indexed-types/should_compile/T14131.hs:29:3: error:
• Type indexes must match class instance head
Expected: ZT k
Actual: ZT k
• In the class declaration for ‘Z’
|
29 | type ZT = (Nothing :: Maybe k)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
}}}
I'm still not sure what's going on here—more investigation is required.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15591#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
More information about the ghc-tickets
mailing list