Opened 3 years ago

Last modified 16 months ago

#13192 new bug

Ambiguity Caused By PolyKind and Not Helpful Error Messages

Reported by: Shayan-Najd Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.1
Keywords: TypeFamilies Cc: simonpj
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Poor/confusing error message Test Case:
Blocked By: Blocking:
Related Tickets: #10789 Differential Rev(s):
Wiki Page:

Description

The following code results in a confusing/wrong error message, blaming a type variable (a) being a fixed Skolem variable:

{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE PolyKinds              #-}

data I a

type family   F  x
type instance F  (I a) = a

identity :: F (I a) -> F (I a)
identity x = x

with the error message

    • Couldn't match type ‘F (I a0)’ with ‘F (I a)’
      Expected type: F (I a) -> F (I a)
        Actual type: F (I a0) -> F (I a0)
      NB: ‘F’ is a type function, and may not be injective
      The type variable ‘a0’ is ambiguous
    • In the ambiguity check for ‘identity’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature: identity :: F (I a) -> F (I a)
  |
9 | identity :: F (I a) -> F (I a)
  |             ^^^^^^^^^^^^^^^^^^

Change History (6)

comment:1 Changed 3 years ago by goldfire

To add more information: this code is accepted without PolyKinds, because F (I a) can immediately reduce to a. With PolyKinds, F (I a) is stuck, as we don't know a's kind. (The equation for F works only when (a :: Type).)

Perhaps the best fix is to add a check in TcErrors for type families that match on invisible parameters (i.e., kinds) and emit a NB: Type family `F' has equations that depend on the kind of its argument(s).

comment:2 Changed 3 years ago by rwbarton

Why does it also not work if I change the definition of F to

type family   F  (x :: *) :: k

in which case ghci tells me the instance is

type instance F k (I k a) = a   -- Defined at I.hs:7:16

but ghc gives the same error regarding identity. Is k not determined by the result kind of the type family, i.e., the fact that F (I a) appears as a type argument to (->)?

comment:3 Changed 3 years ago by simonpj

Can you explain more precisely why F (I a) is stuck with PolyKinds? I don't get it.

comment:4 Changed 3 years ago by rwbarton

In the original program, the application F (I a) is stuck because

  • data I a really means data I k (a :: k) :: *, i.e., I is polykinded
  • type family F x really means type family F k (x :: *) :: *, i.e., F is not polykinded
  • type instance F (I a) = a really means type instance F (I * a) = a, because the instance is only well-kinded when a has kind *.

But there's nothing stopping one from adding an additional instance type instance F (I Maybe) = Char which uses I at a different kind.

  • identity :: F (I a) -> F (I a) really means identity :: forall k (a :: k). F (I k a) -> F (I k a), i.e., identity is polykinded. Now there's a problem because the instance we defined only applies when k = *, but here k could really be anything, like * -> *.

And indeed if I added the type instance F (I Maybe) = Char, then I can write identity @ Maybe and it has type Char -> Char just like identity @ Char does. So the type really is ambiguous.

What I'm confused about is why F (I a) is still stuck even when I make the result of F polykinded, so that the instance type instance F (I a) = a applies at all kinds.

comment:5 Changed 3 years ago by goldfire

The type instance in @rwbarton's case expands to F k (I k a) = a. This instance requires the two ks to be the same. In identity's type signature, we get F (TYPE r) (I k a) -> F (TYPE r') (I k a). GHC (rightly) doesn't know that k and TYPE r are the same. (The fact that it's TYPE r and not Type is not the issue.)

comment:6 Changed 16 months ago by RyanGlScott

Keywords: TypeFamilies added
Note: See TracTickets for help on using tickets.