[GHC] #16374: Cannot deduce constraint from itself with poly-kinded type family

[GHC]

#16374: Cannot deduce constraint from itself with poly-kinded type family
-------------------------------------+-------------------------------------
        Reporter:  roland            |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler (Type    |              Version:  8.6.3
  checker)                           |
      Resolution:                    |             Keywords:
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):

 Enabling `-fprint-explicit-kinds` reveals in greater detail what is
 happening here:

 {{{
 $ ~/Software/ghc-gitlab/inplace/bin/ghc-stage2 --interactive Bug.hs
 -fprint-explicit-kinds
 GHCi, version 8.9.20190227: https://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Eq               ( Bug.hs, interpreted )

 Bug.hs:7:11: error:
     • Could not deduce: (F @{*} @k0 Int :: k0)
                         ~ (F @{*} @k0 Bool :: k0)
       from the context: (F @{*} @k Int :: k) ~ (F @{*} @k Bool :: k)
         bound by the type signature for:
                    withEq :: forall k a.
                              ((F @{*} @k Int :: k) ~ (F @{*} @k Bool ::
 k)) =>
                              a
         at Bug.hs:7:11-29
       NB: ‘F’ is a non-injective type family
       The type variable ‘k0’ is ambiguous
     • In the ambiguity check for ‘withEq’
       To defer the ambiguity check to use sites, enable
 AllowAmbiguousTypes
       In the type signature: withEq :: F Int ~ F Bool => a
   |
 7 | withEq :: F Int ~ F Bool => a
   |           ^^^^^^^^^^^^^^^^^^^
 }}}

 Here, we can see exactly where the ambiguous kind variable `k0` occurs.

 It might be helpful to have GHC automatically enable `-fprint-explicit-
 kinds` is an ambiguous type variable occurs in a kind position, such as in
 this program. We already do this in a number of places, such as when
 [https://gitlab.haskell.org/ghc/ghc/blob/2e8f664957dc3763dc4375894b8dc4d046d2e95b/compiler/typecheck/TcErrors.hs#L1931
 a type mismatch occurs due to kind arguments].

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/16374#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler