#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... 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