#14419: Check kinds for ambiguity -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType 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): Actually, the situation in comment:4 in which a visible, dependent kind is erroneously flagged as ambiguous can occur //today//, even without that patch. Take this program, for example: {{{#!hs {-# LANGUAGE DataKinds #-} {-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE TypeFamilies #-} module Bug where import Data.Kind type KindOf (a :: k) = k type family F a data A (a :: Type) :: F a -> Type data Ex (x :: KindOf A) }}} {{{ $ /opt/ghc/8.6.2/bin/ghc Bug.hs [1 of 1] Compiling Bug ( Bug.hs, Bug.o ) Bug.hs:13:1: error: • Couldn't match type ‘F a’ with ‘F a0’ Expected type: F a -> * Actual type: F a0 -> * NB: ‘F’ is a non-injective type family The type variable ‘a0’ is ambiguous • In the ambiguity check for the kind annotation on the type variable ‘x’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes | 13 | data Ex (x :: KindOf A) | ^^^^^^^^^^^^^^^^^^^^^^^ }}} I believe this should be accepted since `KindOf A` reduces to `forall a -> F a -> Type`, and the `forall a ->` //should// uniquely determine the `a` in `F a`. Alas, GHC doesn't currently recognize this. Thankfully, the workaround for the time being is simple: just enable `AllowAmbiguousTypes`. But I'll go ahead and post this here to make it clear that this is a problem in the present, and not just a problem for a future GHC. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14419#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler