Haskell › Haskell - Glasgow-haskell-bugs

[GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

Classic

List

Threaded

11 messages Options

GHC

[GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

#6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable
---------------------------------------+------------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler
Version: 7.4.1 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------------+------------------------------------
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)))
}}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6015>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

#6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable
---------------------------------------+------------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Component: Compiler
Version: 7.4.1 | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------------+------------------------------------

Comment(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'
}}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6015#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

#6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable
---------------------------------+------------------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid program
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------

Comment(by atnnn):

Replying to [comment:2 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`.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6015#comment:3>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

#6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable
---------------------------------+------------------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: GHC rejects valid program
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------

Comment(by simonpj@…):

commit 6c3045b90fb28861fae826c8bbd53135d3f2a6ce
{{{
Author: Simon Peyton Jones <[hidden email]>
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(-)
}}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6015#comment:4>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

#6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable
----------------------------------------+-----------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Resolution: | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: polykinds/T6015 | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------
Changes (by atnnn):

* status: closed => new
* resolution: fixed =>

Comment:

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
}}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6015#comment:7>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

#6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable
----------------------------------------+-----------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Resolution: | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: polykinds/T6015 | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------

Comment(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?

Simon

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6015#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC

#6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable
----------------------------------------+-----------------------------------
Reporter: atnnn | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.4.1
Resolution: | Keywords:
Os: Unknown/Multiple | Architecture: Unknown/Multiple
Failure: GHC rejects valid program | Difficulty: Unknown
Testcase: polykinds/T6015 | Blockedby:
Blocking: | Related:
----------------------------------------+-----------------------------------

Comment(by simonpj@…):

commit 969f8b728be0a2fec8263e8866295776c993394b
{{{
Author: Simon Peyton Jones <[hidden email]>
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(-)
}}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6015#comment:9>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
Glasgow-haskell-bugs mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs

GHC

Re: [GHC] #6015: "No instance" when using PolyKinds/DataKinds/FunDeps/Undecidable

In reply to this post by GHC