Opened 7 months ago

Last modified 7 months ago

#16374 new bug

Cannot deduce constraint from itself with poly-kinded type family

Reported by: roland Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.6.3
Keywords: TypeErrorMessages Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

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.

Change History (2)

comment:1 Changed 7 months ago 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 a type mismatch occurs due to kind arguments.

comment:2 Changed 7 months ago by simonpj

Keywords: TypeErrorMessages added

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.

I totally agree. Would anyone like to do this?

There are a number of other tickets about improving type error messages

Note: See TracTickets for help on using tickets.