[GHC] #14419: Check kinds for ambiguity

[GHC]

#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