Cannot deduce constraint from itself with poly-kinded type family

Compiling

{-# LANGUAGE PolyKinds, TypeFamilies #-}

module Eq where

type family F a :: k where

withEq :: F Int ~ F Bool => a
withEq = undefined

gives an arguably confusing error message:

Eq.hs:7:11: error:
    • Could not deduce: F Int ~ F Bool
      from the context: F Int ~ F Bool
        bound by the type signature for:
                   withEq :: forall k a. (F Int ~ F Bool) => a
        at Eq.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

I'm not claiming this program should necessarily typecheck, but "Cannot deduce X from the context X" induces head-scratching.

Replacing k with * in the definition of F makes the error go away.

Trac metadata

Trac field	Value
Version	8.6.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture