#9019 closed bug (invalid)

Ambiguity checker overeager on "ambiguous" kind variables

Reported by: goldfire Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.8.2
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

Consider the following shenanigans:

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies,
             ExistentialQuantification #-}

module Bug where

import Data.Proxy

data TyFun :: * -> * -> *
type family Apply (f :: TyFun k1 k2 -> *) (x :: k1) :: k2

data LeftSym0 l =
  forall arg. Apply LeftSym0 arg ~ Left arg => LS0KI (Proxy arg)

Compiling (with -fprint-explicit-foralls -fprint-explicit-kinds) gives this error message:

/Users/rae/temp/Bug.hs:12:3:
    Could not deduce ((~)
                        (Either k3 k0)
                        (Apply (Either k3 k0) k3 (LeftSym0 k0 k3) arg)
                        ('Left k3 k0 arg))
    from the context ((~)
                        (Either k3 k2)
                        (Apply (Either k3 k2) k3 (LeftSym0 k2 k3) arg)
                        ('Left k3 k2 arg))
      bound by the type of the constructor ‘LS0KI’:
                 (~)
                   (Either k3 k2)
                   (Apply (Either k3 k2) k3 (LeftSym0 k2 k3) arg)
                   ('Left k3 k2 arg) =>
                 Proxy k3 arg -> LeftSym0 k k1 l
      at /Users/rae/temp/Bug.hs:12:3
    The type variable ‘k0’ is ambiguous
    In the ambiguity check for:
      forall (k :: BOX)
             (k1 :: BOX)
             (l :: TyFun k1 (Either k1 k))
             (k2 :: BOX)
             (k3 :: BOX)
             (arg :: k3).
      (~)
        (Either k3 k2)
        (Apply (Either k3 k2) k3 (LeftSym0 k2 k3) arg)
        ('Left k3 k2 arg) =>
      Proxy k3 arg -> LeftSym0 k k1 l
    To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
    In the definition of data constructor ‘LS0KI’
    In the data declaration for ‘LeftSym0’

The file compiles without incident with -XAllowAmbiguousTypes.

What's interesting is that, then, the following separate module compiles:

{-# LANGUAGE PolyKinds, DataKinds, TypeFamilies #-}

module B2 where

import Bug
import Data.Proxy

type instance Apply LeftSym0 x = Left x

foo = LS0KI Proxy

It seems that LS0KI's type was not so ambiguous after all.

I would want to reduce the test case, but it's hard to figure out what GHC is thinking here, as it reports an ambiguous k0 variable, which does not appear in the type it is examining. A few rather naive attempts to reduce failed.

Change History (2)

comment:1 Changed 12 months ago by simonpj

Sure it's ambiguous! Try

lsoki :: Apply LeftSym0 arg ~ Left arg => Proxy arg -> LeftSym0 l
lsoki = LSOKI

and you get the exact same error message. "Ambiguous" does not mean "can never under any circumstances be called".

Here's a simpler example:

class C (x :: Maybe a)

data LeftSym0 where
  LSOKI :: C Nothing => LeftSym0

This gives

T9019.hs:9:3:
    Could not deduce (C k0 ('Nothing k0))
      arising from the ambiguity check for the type of the constructor ‘LSOKI’
    from the context (C k ('Nothing k))
      bound by the type of the constructor ‘LSOKI’:
                 C k ('Nothing k) => LeftSym0
      at T9019.hs:9:3
    The type variable ‘k0’ is ambiguous
    In the ambiguity check for:
      forall (k :: BOX). C k ('Nothing k) => LeftSym0

And indeed, there is nothing to resolve that ambiguous 'k', just as there wasn't in the previous example.

So this looks right to me.

Simon

comment:2 Changed 11 months ago by goldfire

  • Resolution set to invalid
  • Status changed from new to closed

I suppose you're right. I was under the assumption that ambiguous types can never be called, in exact contradiction to what is in the user manual.

Thanks for taking the time to correct me!

Note: See TracTickets for help on using tickets.