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

1 Mar 2019

      #16374: Cannot deduce constraint from itself with poly-kinded type family
-------------------------------------+-------------------------------------
           Reporter:  roland         |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.6.3
  (Type checker)                     |
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Compiling
 {{{#!hs
 {-# 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.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16374
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler