Opened 4 years ago

Closed 4 years ago

#6015 closed feature request (fixed)

"No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

Reported by: atnnn Owned by:
Priority: normal Milestone:
Component: Compiler Version: 7.4.1
Keywords: Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case: polykinds/T6015, T6015a
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


Consider this GHCi session:

> value (Proxy :: Proxy (Just True))
No instance for (Value (Maybe Bool) (Just Bool 'True) t0)
> :i Value
instance Value Bool 'True Bool
instance Value k a t => Value (Maybe k) (Just k a) (Maybe t)
> value (Proxy :: Proxy (Just True)) :: Maybe Bool
Just True

It would be helpful if GHC could use the instance (which seems suitable) or emit a better error message.

{-# LANGUAGE DataKinds, MultiParamTypeClasses, FunctionalDependencies,
             PolyKinds, UndecidableInstances, ScopedTypeVariables #-}

data Proxy a = Proxy
class Value a t | a -> t where value :: Proxy a -> t
instance Value True Bool where value _ = True
instance Value a t => Value (Just a) (Maybe t)
    where value _ = Just (value (Proxy :: Proxy a))

-- main = print (value (Proxy :: Proxy (Just True)))

Attachments (1)

substkind-6015.patch (764 bytes) - added by atnnn 4 years ago.

Download all attachments as: .zip

Change History (11)

comment:1 Changed 4 years ago by atnnn

I have been poking at the GHC source to see if I can get this to typecheck. Here is a simpler example that does not use DataKinds or UndecidableInstances.

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}

-- {-# LANGUAGE PolyKinds #-}

class Foo a b | a -> b
instance Foo a ()

foo :: Foo () b => b
foo = undefined

Without PolyKinds, GHCi doesn't complain about the type

>>> foo
*** Exception: Prelude.undefined

Uncommenting the PolyKinds pragma makes GHCi complain.

>>> foo
No instance for (Foo * * () b0) arising from a use of `foo'

comment:2 follow-up: Changed 4 years ago by simonpj

  • difficulty set to Unknown

That's odd. Even with PolyKinds on the program typechecks for me. Are you using the latest HEAD?

But still there's a bug in 6015, and I think I know what it is. I'll try to fix it today.


comment:3 in reply to: ↑ 2 Changed 4 years ago by atnnn

Replying to simonpj:

That's odd. Even with PolyKinds on the program typechecks for me. Are you using the latest HEAD?

I tried again with the latest HEAD.

As before, the code compiles fine and the No instance error appears only when trying to evaluate foo.

Also, I forgot to add the required FlexibleContexts.

comment:4 Changed 4 years ago by simonpj@…

commit 6c3045b90fb28861fae826c8bbd53135d3f2a6ce

Author: Simon Peyton Jones <[email protected]>
Date:   Mon May 14 14:05:48 2012 +0100

    Fix the the pure unifier so that it unifies kinds
    When unifying two type variables we must unify their kinds.
    The pure *matcher* was doing so, but the pure *unifier* was not.
    This patch fixes Trac #6015, where an instance lookup was failing
    when it should have succeeded.
    I removed a bunch of code aimed at support sub-kinding. It's
    tricky, ad-hoc, and I don't think its necessary any more.
    Anything we can do to simplify the sub-kinding story is welcome!

 compiler/types/FunDeps.lhs |    4 +++
 compiler/types/Unify.lhs   |   50 +++++++++++++++----------------------------
 2 files changed, 22 insertions(+), 32 deletions(-)

comment:5 Changed 4 years ago by simonpj

  • Test Case set to polykinds/T6015

Thanks for a nicely-characterised error. Now fixed.

comment:6 Changed 4 years ago by simonpj

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

comment:7 Changed 4 years ago by atnnn

  • Resolution fixed deleted
  • Status changed from closed to new

Thanks Simon.

Here is an extra one line patch that substitutes the kind variables that your fix now let's through. Without it, the following code panics.

{-# LANGUAGE PolyKinds, KindSignatures, FunctionalDependencies, FlexibleInstances,
             UndecidableInstances, TypeOperators, DataKinds, FlexibleContexts #-}

import Prelude hiding ((++))

data T a = T

class ((a :: [k]) ++ (b :: [k])) (c :: [k]) | a b -> c
instance ('[] ++ b) b
instance (a ++ b) c => ((x ': a) ++ b) (x ': c)

test = T :: ('[True] ++ '[]) l => T l

This may be what the TODO in TcInteract.instFunDepEqn is about.

       ; tys' <- mapM instFlexiTcS tvs  -- IA0_TODO: we might need to do kind substitution

Changed 4 years ago by atnnn

comment:8 Changed 4 years ago by simonpj

Whoa! atnnn, you are right on the ball. I'd found this exact same problem when looking at #6068, but it's a subtle one. So hats off you to you for finding the exact spot where the bug is. (Took me a little while.)

Feel free to keep debugging type inference! You clearly know what you are doing. I wonder who you really are?


comment:9 Changed 4 years ago by simonpj@…

commit 969f8b728be0a2fec8263e8866295776c993394b

Author: Simon Peyton Jones <[email protected]>
Date:   Wed May 16 11:13:52 2012 +0100

    Be careful to instantiate kind variables when dealing with functional dependencies
    There were really two bugs
      a) When the fundep fires we must apply the matching
         substitution to the kinds of the remaining type vars
         (This happens in FunDeps.checkClsFD, when we create meta_tvs)
      b) When instantiating the un-matched type variables we must
         instantiate their kinds properly
         (This happens in TcSMonad.instFlexiTcS)
    This fixes #6068 and #6015 (second reported bug).

 compiler/typecheck/TcInteract.lhs |    6 +--
 compiler/typecheck/TcSMonad.lhs   |    8 +++-
 compiler/types/FunDeps.lhs        |   87 ++++++++++++++++++++++---------------
 3 files changed, 60 insertions(+), 41 deletions(-)

comment:10 Changed 4 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case changed from polykinds/T6015 to polykinds/T6015, T6015a

I believe this patch fixes the bug. Thanks for reporting it with a nice small test case. Give it a try


Note: See TracTickets for help on using tickets.