#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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): OK, I think I know what is going on here. The reason that neither of these declarations: {{{#!hs data T2 :: F a -> Type data T3 (b :: F a) }}} Were flagged as ambiguously kinded is because `checkValidType` was only being called on the kinds of the individual arguments and result. In the former case, that would be `F a[sk] -> Type`, and in the latter case, it would be `F a[sig]`. What we need to be doing to catch the ambiguity in those cases is to call `checkValidType` on the //entire// kind of the declaration—in both cases, `forall a. F a -> Type`. I even whipped up a patch for doing so, which is essentially as simple as sticking an extra check in `kcTyClGroup`: {{{#!diff diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs index 7e523a7..2d4dfc5 100644 --- a/compiler/typecheck/TcTyClsDecls.hs +++ b/compiler/typecheck/TcTyClsDecls.hs @@ -535,10 +535,13 @@ kcTyClGroup decls ; checkValidTelescope all_binders user_tyvars extra -- Make sure tc_kind' has the final, zonked kind variables + ; let tc_kind' = mkTyConKind all_binders' tc_res_kind' + ; checkValidType (DeclKindCtxt name) tc_kind' + ; traceTc "Generalise kind" $ vcat [ ppr name, ppr tc_binders, ppr (mkTyConKind tc_binders tc_res_kind) , ppr kvs, ppr all_binders, ppr tc_res_kind - , ppr all_binders', ppr tc_res_kind' + , ppr all_binders', ppr tc_res_kind', ppr tc_kind' , ppr scoped_tvs ] ; return (mkTcTyCon name user_tyvars all_binders' tc_res_kind' }}} That catches both of the examples above. But there's a gotcha that I didn't anticipate: consider these: {{{#!hs {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeInType #-} module Bug where type family F (x :: a) type family T1 (x :: a) :: F a -- Kind: forall a. a -> F a type family T2 (x :: a) :: F x -- Kind: forall a. forall (x :: a) -> F x }}} After my patch, GHC flags `T2` as ambiguous: {{{ $ ghc/inplace/bin/ghc-stage2 --interactive Bug.hs GHCi, version 8.5.20180521: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Bug ( Bug.hs, interpreted ) Bug.hs:8:1: error: • Couldn't match expected type ‘F x’ with actual type ‘F x0’ NB: ‘F’ is a non-injective type family The type variable ‘x0’ is ambiguous • In the ambiguity check for the top-level kind for ‘T2’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type family declaration for ‘T2’ | 8 | type family T2 (x :: a) :: F x | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ }}} I find this somewhat surprising, since I would expect that the `forall (x :: a)` argument in the kind of `T2` would fully determine `x`. Perhaps this is a deficiency in the code which checks for ambiguity? I tried taking a look myself, but quickly became lost, since it relies on `tcSubType_NC` (something that is completely impenetrable to me). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler