Quantcast

[GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

classic Classic list List threaded Threaded
6 messages Options
GHC
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

[GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

GHC
#6020: "Couldn't match kind" with free type variables and PolyKinds
---------------------------------------+------------------------------------
 Reporter:  atnnn                      |          Owner:                  
     Type:  feature request            |         Status:  new            
 Priority:  normal                     |      Component:  Compiler        
  Version:  7.5                        |       Keywords:                  
       Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
  Failure:  GHC rejects valid program  |       Testcase:                  
Blockedby:                             |       Blocking:                  
  Related:                             |  
---------------------------------------+------------------------------------
 In the following code, I was hoping that GHC could infer the more specific
 kind of the free variable y and the class Id in the head of the instance
 for Test.

 Also, the error message is confusing:

 - It says that 'True has kind k0 (maybe it's an impredicative kind?)

 - It refers to k0 as a type variable

 {{{

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

 import GHC.Prim (Constraint)

 class Id (a :: k) (b :: k) | a -> b
 instance Id a a

 class Test (x :: a) (y :: a) | x -> y
 instance (Id x y, Id y z) => Test x z

 test :: Test True True => ()
 test = ()
 }}}

 {{{
 >>> test
 <interactive>:54:1:
     Couldn't match kind `k0' with `Bool'
       `k0' is an unknown type variable
     Kind incompatibility when matching types:
       'True :: k0
       'True :: Bool
     When using functional dependencies to combine
       Id k0 a a,
         arising from the dependency `a -> b'
         in the instance declaration at /home/atnnn/code/type-
 prelude/testfoldl.hs:8:10
       Id Bool 'True 'True,
         arising from a use of `test' at <interactive>:54:1-4
     In the expression: test
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020>
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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

GHC
#6020: "Couldn't match kind" with free type variables and PolyKinds
---------------------------------------+------------------------------------
 Reporter:  atnnn                      |          Owner:                  
     Type:  feature request            |         Status:  new            
 Priority:  normal                     |      Component:  Compiler        
  Version:  7.5                        |       Keywords:                  
       Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
  Failure:  GHC rejects valid program  |       Testcase:                  
Blockedby:                             |       Blocking:                  
  Related:                             |  
---------------------------------------+------------------------------------

Comment(by atnnn):

 Pinning the kind makes the instance work:

 {{{
 instance (Id x y, Id y z) => Test x (z :: Bool)
 }}}

 But using kind variables doesn't:

 {{{
 instance (Id x (y :: k), Id y z) => Test x (z :: k)
 }}}

 {{{
 Not in scope: type variable `k'
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020#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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

GHC
In reply to this post by GHC
#6020: "Couldn't match kind" with free type variables and PolyKinds
---------------------------------------+------------------------------------
 Reporter:  atnnn                      |          Owner:                  
     Type:  feature request            |         Status:  new            
 Priority:  normal                     |      Component:  Compiler        
  Version:  7.5                        |       Keywords:                  
       Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
  Failure:  GHC rejects valid program  |       Testcase:                  
Blockedby:                             |       Blocking:                  
  Related:                             |  
---------------------------------------+------------------------------------

Comment(by simonpj@…):

 commit 6b0537a13b101755d9f2b807e32751845ada6c4f
 {{{
 Author: Simon Peyton Jones <[hidden email]>
 Date:   Sun Apr 22 17:52:55 2012 +0100

     Respect kind-variable scoping when instantiating dfuns

     Fixes Trac #6020

  compiler/typecheck/TcInteract.lhs |   17 +++++---------
  compiler/typecheck/TcSMonad.lhs   |   44
 +++++++++++++++++++++---------------
  compiler/types/InstEnv.lhs        |   34 +++++++++++++---------------
  3 files changed, 48 insertions(+), 47 deletions(-)
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020#comment:2>
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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

GHC
In reply to this post by GHC
#6020: "Couldn't match kind" with free type variables and PolyKinds
----------------------------------------+-----------------------------------
  Reporter:  atnnn                      |          Owner:                  
      Type:  feature request            |         Status:  closed          
  Priority:  normal                     |      Milestone:                  
 Component:  Compiler                   |        Version:  7.5            
Resolution:  fixed                      |       Keywords:                  
        Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
   Failure:  GHC rejects valid program  |     Difficulty:  Unknown        
  Testcase:  polykinds/T6020            |      Blockedby:                  
  Blocking:                             |        Related:                  
----------------------------------------+-----------------------------------
Changes (by simonpj):

  * status:  new => closed
  * difficulty:  => Unknown
  * resolution:  => fixed
  * testcase:  => polykinds/T6020


Comment:

 Thanks.  Fixed.

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020#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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

GHC
In reply to this post by GHC
#6020: "Couldn't match kind" with free type variables and PolyKinds
----------------------------------------+-----------------------------------
  Reporter:  atnnn                      |          Owner:                  
      Type:  feature request            |         Status:  new            
  Priority:  normal                     |      Milestone:                  
 Component:  Compiler                   |        Version:  7.5            
Resolution:                             |       Keywords:                  
        Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
   Failure:  GHC rejects valid program  |     Difficulty:  Unknown        
  Testcase:  polykinds/T6020            |      Blockedby:                  
  Blocking:                             |        Related:                  
----------------------------------------+-----------------------------------
Changes (by atnnn):

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


Comment:

 If I switch to equality constraints and reverse the functional dependency
 of Id, I get the same error as above ({{{Couldn't match kind `k0' with
 `Bool'}}}):

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

 class Id (a :: k) (b :: k) | b -> a
 instance a ~ b => Id a b

 class Test (x :: a) (y :: a)
 instance (Id x y, Id y z) => Test x z

 test :: Test True True => ()
 test = ()

 main = print test
 }}}

 If I comment out `main`, it loads fine but GHC now panics when I use
 `test`:

 {{{
 >>> :load "testid.hs"
 >>> test
 ghc-stage2: panic! (the 'impossible' happened)
   (GHC version 7.5.20120425 for x86_64-unknown-linux):
         tcTyVarDetails k0{tv alS} [tv]
 }}}

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020#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
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Re: [GHC] #6020: "Couldn't match kind" with free type variables and PolyKinds

GHC
In reply to this post by GHC
#6020: "Couldn't match kind" with free type variables and PolyKinds
----------------------------------------+-----------------------------------
  Reporter:  atnnn                      |          Owner:                  
      Type:  feature request            |         Status:  closed          
  Priority:  normal                     |      Milestone:                  
 Component:  Compiler                   |        Version:  7.5            
Resolution:  fixed                      |       Keywords:                  
        Os:  Unknown/Multiple           |   Architecture:  Unknown/Multiple
   Failure:  GHC rejects valid program  |     Difficulty:  Unknown        
  Testcase:  polykinds/T6020, T6020a    |      Blockedby:                  
  Blocking:                             |        Related:                  
----------------------------------------+-----------------------------------
Changes (by simonpj):

  * status:  new => closed
  * testcase:  polykinds/T6020 => polykinds/T6020, T6020a
  * resolution:  => fixed


Comment:

 Urgh.  A one-character typo! Fixed by
 {{{
 commit 4cc882650af6a4fadb30706f21e987edb846bcc3
 Author: Simon Peyton Jones <[hidden email]>
 Date:   Thu Apr 26 09:29:15 2012 +0100

     Fix a one-character typo (kv1 should be kv2!)

     Fixes Trac #6020, #6044
 >---------------------------------------------------------------

  compiler/typecheck/TcUnify.lhs |    2 +-
  1 files changed, 1 insertions(+), 1 deletions(-)

 diff --git a/compiler/typecheck/TcUnify.lhs
 b/compiler/typecheck/TcUnify.lhs index 1729dcd..6e4d128 100644
 --- a/compiler/typecheck/TcUnify.lhs
 +++ b/compiler/typecheck/TcUnify.lhs
 @@ -1119,7 +1119,7 @@ uKVar isFlipped unify_kind eq_res kv1 k2
    | TyVarTy kv2 <- k2, kv1 == kv2
    = return eq_res

 -  | TyVarTy kv2 <- k2, isTcTyVar kv1, isMetaTyVar kv2
 +  | TyVarTy kv2 <- k2, isTcTyVar kv2, isMetaTyVar kv2
    = uKVar (not isFlipped) unify_kind eq_res kv2 (TyVarTy kv1)

    | otherwise = if isFlipped
 }}}
 I added a new regression test too!

--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6020#comment:5>
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
Loading...