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

#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

#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/2e8f664957dc3763dc4375894b8dc4d046d2... 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

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
#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) | Keywords: Resolution: | TypeErrorMessages Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by simonpj): * keywords: => TypeErrorMessages Comment: this program. I totally agree. Would anyone like to do this? There are a number of other [wiki:Status/TypeErrorMessages tickets about improving type error messages] -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16374#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC