GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=!closed&reporter=kosmikus&order=priority
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?status=!closed&reporter=kosmikus&order=priority
Trac 1.0.1
http://ghc.haskell.org/trac/ghc/ticket/8966
http://ghc.haskell.org/trac/ghc/ticket/8966#8966: Pattern synonyms and kind-polymorphismMon, 07 Apr 2014 12:59:03 GMTkosmikus<p>
There's a strange interaction between pattern synonyms, GADTs, kind polymorphism and data kinds.
</p>
<p>
The following module fails to compile with ghc-7.8.1-rc2, but I think it should:
</p>
<pre class="wiki">{-# LANGUAGE PolyKinds, KindSignatures, PatternSynonyms, DataKinds, GADTs #-}
data NQ :: [k] -> * where
D :: NQ '[a]
pattern Q = D
</pre><p>
I get the following error:
</p>
<pre class="wiki">KindPat.hs:6:13:
Could not deduce (a ~ a0)
from the context (t ~ '[a])
bound by the type signature for (Main.$WQ) :: t ~ '[a] => NQ t
at KindPat.hs:6:9
‘a’ is a rigid type variable bound by
the type signature for (Main.$WQ) :: t ~ '[a] => NQ t
at KindPat.hs:6:13
Expected type: NQ t
Actual type: NQ '[a0]
In the expression: D
In an equation for ‘$WQ’: ($WQ) = D
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/8966#changelog
http://ghc.haskell.org/trac/ghc/ticket/8968
http://ghc.haskell.org/trac/ghc/ticket/8968#8968: Pattern synonyms and GADTsMon, 07 Apr 2014 15:36:35 GMTkosmikus<p>
I think this one is different from <a class="merge ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8966" title="bug: Pattern synonyms and kind-polymorphism (merge)">#8966</a>, but feel free to close one as duplicate if it turns out to be the same problem.
</p>
<p>
The following program (using GADTs and pattern synonyms, but not kind polymorphism or data kinds) fails to check with ghc-7.8.1-rc2, but I think it should:
</p>
<pre class="wiki">{-# LANGUAGE GADTs, KindSignatures, PatternSynonyms #-}
data X :: (* -> *) -> * -> * where
Y :: f Int -> X f Int
pattern C x = Y (Just x)
</pre><p>
The error I get is the following:
</p>
<pre class="wiki">PatKind.hs:6:18:
Couldn't match type ‘t’ with ‘Maybe’
‘t’ is untouchable
inside the constraints (t1 ~ Int)
bound by a pattern with constructor
Y :: forall (f :: * -> *). f Int -> X f Int,
in a pattern synonym declaration
at PatKind.hs:6:15-24
‘t’ is a rigid type variable bound by
the inferred type of
C :: X t t1
x :: Int
at PatKind.hs:1:1
Expected type: t Int
Actual type: Maybe Int
In the pattern: Just x
In the pattern: Y (Just x)
PatKind.hs:6:18:
Could not deduce (t ~ Maybe)
from the context (t1 ~ Int)
bound by the type signature for
(Main.$WC) :: t1 ~ Int => Int -> X t t1
at PatKind.hs:6:9
‘t’ is a rigid type variable bound by
the type signature for (Main.$WC) :: t1 ~ Int => Int -> X t t1
at PatKind.hs:1:1
Expected type: t Int
Actual type: Maybe Int
Relevant bindings include
($WC) :: Int -> X t t1 (bound at PatKind.hs:6:9)
In the first argument of ‘Y’, namely ‘(Just x)’
In the expression: Y (Just x)
</pre><p>
Note that I'd be perfectly happy to provide a type signature for the pattern synonym, but I don't know of any syntax I could use. The Wiki page at <a class="ext-link" href="https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms"><span class="icon"></span>https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms</a> mentions I might be able to write
</p>
<pre class="wiki">pattern C :: Int -> X Maybe Int
</pre><p>
but this triggers a parse error.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8968#changelog
http://ghc.haskell.org/trac/ghc/ticket/8985
http://ghc.haskell.org/trac/ghc/ticket/8985#8985: Strange kind error with type family, GADTs, data kinds, and kind polymorphismFri, 11 Apr 2014 07:16:52 GMTkosmikus<p>
Consider the following test case (I've tried hard to make it minimal, which unfortunately means there's not a lot of intuition left):
</p>
<pre class="wiki">{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators #-}
data X (xs :: [k]) = MkX
data Y :: (k -> *) -> [k] -> * where
MkY :: f x -> Y f (x ': xs)
type family F (a :: [[*]]) :: *
type instance F xss = Y X xss
works :: Y X '[ '[ ] ] -> ()
works (MkY MkX) = ()
fails :: F '[ '[ ] ] -> ()
fails (MkY MkX) = ()
</pre><p>
This code compiles in GHC 7.6.3, but it fails in GHC 7.8.1 (both rc2 and the actual release) with the following error:
</p>
<pre class="wiki">TestCase.hs:14:8:
Couldn't match kind ‘k0’ with ‘*’
Expected type: F '['[]]
Actual type: Y t0 t1
In the pattern: MkY MkX
In an equation for ‘fails’: fails (MkY MkX) = ()
TestCase.hs:14:12:
Couldn't match type ‘t0’ with ‘X’
‘t0’ is untouchable
inside the constraints (t1 ~ (x : xs))
bound by a pattern with constructor
MkY :: forall (f :: k -> *) (x :: k) (xs :: [k]).
f x -> Y f (x : xs),
in an equation for ‘fails’
at TestCase.hs:14:8-14
Expected type: t0 x
Actual type: X x
In the pattern: MkX
In the pattern: MkY MkX
In an equation for ‘fails’: fails (MkY MkX) = ()
</pre><p>
I'm puzzled that simply adding the type family invokation makes the type checker fail with a kind error, even though the type family itself itsn't kind-polymorphic.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8985#changelog