GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=!closed&component=Compiler+(Type+checker)&desc=1&order=id
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?status=!closed&component=Compiler+(Type+checker)&desc=1&order=id
Trac 1.0.1
http://ghc.haskell.org/trac/ghc/ticket/9014
http://ghc.haskell.org/trac/ghc/ticket/9014#9014: GHC 7.8.2 Win64 tarball includes gfortran/gcj/pythonSun, 20 Apr 2014 17:37:02 GMTrefold<p>
The released Windows 64 tarball available at <a class="ext-link" href="https://www.haskell.org/ghc/dist/7.8.2/ghc-7.8.2-x86_64-unknown-mingw32.tar.xz"><span class="icon"></span>https://www.haskell.org/ghc/dist/7.8.2/ghc-7.8.2-x86_64-unknown-mingw32.tar.xz</a> includes the following under <tt>mingw/bin</tt>:
</p>
<ul><li>gfortran
</li><li>gcj
</li><li>python27.dll
</li><li>The whole Python 2.7 standard library (<tt>mingw/bin/lib</tt>)
</li></ul><p>
These files have probably been included by mistake.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/9014#changelog
http://ghc.haskell.org/trac/ghc/ticket/8988
http://ghc.haskell.org/trac/ghc/ticket/8988#8988: Documentation build fails if GHCi is unavailableFri, 11 Apr 2014 20:11:04 GMTcjwatson<p>
Joachim Breitner <a class="ext-link" href="http://www.haskell.org/pipermail/glasgow-haskell-users/2014-March/024730.html"><span class="icon"></span>reported</a> that the documentation fails to build on Debian armhf:
</p>
<pre class="wiki"> 0% ( 0 / 5) in 'WwLib'
0% ( 0 / 2) in 'DmdAnal'
0% ( 0 / 2) in 'WorkWrap'
compiler/typecheck/TcSplice.lhs-boot:29:1:
TcSplice.tcTopSpliceExpr is exported by the hs-boot file, but not exported by the module
compiler/typecheck/TcSplice.lhs-boot:37:1:
TcSplice.runMetaE is exported by the hs-boot file, but not exported by the module
compiler/typecheck/TcSplice.lhs-boot:38:1:
TcSplice.runMetaP is exported by the hs-boot file, but not exported by the module
compiler/typecheck/TcSplice.lhs-boot:39:1:
TcSplice.runMetaT is exported by the hs-boot file, but not exported by the module
compiler/typecheck/TcSplice.lhs-boot:40:1:
TcSplice.runMetaD is exported by the hs-boot file, but not exported by the module
67% ( 2 / 3) in 'CmmPipeline'
0% ( 0 / 3) in 'StgCmmHpc'
0% ( 0 / 13) in 'PrelInfo'
0% ( 0 / 4) in 'StgCmmCon'
0% ( 0 / 2) in 'StgCmmExpr'
0% ( 0 / 6) in 'StgCmmBind'
0% ( 0 / 2) in 'CmmParse'
0% ( 0 / 2) in 'StgCmm'
5% ( 9 /175) in 'TcRnMonad'
make[2]: *** [compiler/stage2/doc/html/ghc/ghc.haddock] Error 1
</pre><p>
The attached patch fixes this.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8988#changelog
http://ghc.haskell.org/trac/ghc/ticket/8984
http://ghc.haskell.org/trac/ghc/ticket/8984#8984: Improve output of failed GeneralizedNewtypeDeriving coercion due to type rolesFri, 11 Apr 2014 01:57:12 GMThaasn<p>
When trying to build acme-schoenfinkel (as an example), I came across an error like this:
</p>
<pre class="wiki">Control/Category/Schoenfinkel.hs:66:48:
Could not coerce from ‘cat (cat b c,
b) c’ to ‘cat (WrappedSchoenfinkel cat b c, b) c’
because ‘cat (cat b c, b) c’ and ‘cat (WrappedSchoenfinkel cat b c,
b) c’ are different types.
arising from the coercion of the method ‘app’ from type
‘forall b c. cat (cat b c, b) c’ to type
‘forall b c.
WrappedSchoenfinkel cat (WrappedSchoenfinkel cat b c, b) c’
Possible fix:
use a standalone 'deriving instance' declaration,
so you can specify the instance context yourself
When deriving the instance for (ArrowApply
(WrappedSchoenfinkel cat))
</pre><p>
It was not immediately clear to me as a user that this was caused due to it wanting GNT which was now being blocked by type roles (rightfully so, as this instance allows <tt>UnsafeCoerce</tt>!), and beyond that, what the specific rule that triggered this was.
</p>
<p>
In this case the failure is due to <tt>WrappedSchoenfinkel cat b c</tt> not being nominally equal to <tt>cat b c</tt>, in the type <tt>(WrappedSchoenfinkel cat b c, b)</tt>, which is required to be nominally equal to <tt>(cat b c, b)</tt> because it's used as a parameter to the variable <tt>cat</tt>.
</p>
<p>
Printing a location breakdown and context information similar to this to the user would help understanding and debugging roles a lot.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8984#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="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8966" title="bug: Pattern synonyms and kind-polymorphism (closed: fixed)">#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/8914
http://ghc.haskell.org/trac/ghc/ticket/8914#8914: Remove unnecessary constraints from MonadComprehensions and ParallelListCompWed, 19 Mar 2014 16:29:32 GMTIceland_jack<p>
Many parts of <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/MonadComprehensions">MonadComprehensions</a> don't actually require monads instance, the following could do with a <tt>Functor</tt> constraint
</p>
<pre class="wiki">fmapM :: Monad m => (a -> b) -> m a -> m b
fmapM f xs = [ f x | x <- xs ]
</pre><p>
and I don't see any reason why the class <tt>MonadZip</tt> (from <a class="ext-link" href="http://hackage.haskell.org/package/base-4.4.0.0/docs/Control-Monad-Zip.html"><span class="icon"></span>Control.Monad.Zip</a>) requires a <tt>Monad</tt> constraint rather a <tt>Functor</tt> constraint:
</p>
<pre class="wiki">class Functor f => FunctorZip f where
fzip :: f a -> f b -> f (a,b)
fzip = fzipWith (,)
fzipWith :: (a -> b -> c) -> f a -> f b -> f c
fzipWith f fa fb = fmap (uncurry f) (fzip fa fb)
funzip :: f (a,b) -> (f a, f b)
funzip fab = (fmap fst fab, fmap snd fab)
</pre><p>
with the laws
</p>
<pre class="wiki"> fmap (f *** g) (fzip fa fb) = fzip (fmap f fa) (fmap g fb)
fmap (const ()) fa = fmap (const ()) fb
==> funzip (fzip fa fb) = (fa, fb)
</pre><p>
Same with <tt>Applicative</tt> (see <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/ApplicativeDo">ApplicativeDo</a>):
</p>
<pre class="wiki">liftA2 :: Applicative f => (a -> b -> c) -> f a -> f b -> f c
liftA2 f a1 a2 = [ f x1 x2 | x1 <- a1, x2 <- a2 ]
</pre><p>
The reason I bring this up is because I'm writing a DSL that uses length-indexed vectors whose <tt>Functor</tt> and <tt>FunctorZip</tt> instances are trivial but whose <tt>Monad</tt> instance is <a class="ext-link" href="http://stackoverflow.com/questions/5802628/monad-instance-of-a-number-parameterised-vector"><span class="icon"></span>complicated</a> and not need.
</p>
<p>
This proposal shares a similar rationale as <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/ApplicativeDo">ApplicativeDo</a>.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8914#changelog
http://ghc.haskell.org/trac/ghc/ticket/8907
http://ghc.haskell.org/trac/ghc/ticket/8907#8907: Un-zonked kind variable passes through type checkerMon, 17 Mar 2014 20:24:51 GMTgoldfire<p>
I have this module:
</p>
<pre class="wiki">{-# LANGUAGE PolyKinds #-}
module Bug where
data Poly a
</pre><p>
Now, I say this:
</p>
<pre class="wiki">> ghc Bug.hs -fforce-recomp -dppr-debug -fprint-explicit-foralls -ddump-tc
</pre><p>
The following is produced:
</p>
<pre class="wiki">[1 of 1] Compiling Bug ( Bug.hs, Bug.o )
TYPE SIGNATURES
TYPE CONSTRUCTORS
main:Bug.Poly{tc rn2} :: k{tv ao6} [sk]
-> ghc-prim:GHC.Prim.*{(w) tc 34d}
data Poly{tc} (k::ghc-prim:GHC.Prim.BOX{(w) tc 347}) (a::k)
No C type associated
Roles: [nominal, phantom]
RecFlag NonRecursive, Not promotable
=
FamilyInstance: none
COERCION AXIOMS
Dependent modules: []
Dependent packages: [base, ghc-prim, integer-gmp]
==================== Typechecker ====================
</pre><p>
My concern is the <tt>[sk]</tt> that appears after the kind variable <tt>k_ao6</tt>. It would appear that a <em>skolem</em> type variable passes out of the type-checker and is used as the binder for polymorphic kind of <tt>Poly</tt>. Should this get zonked somewhere?
</p>
<p>
My guess is that there is no way to get this apparent misbehavior to trigger some real failure, given that the variable will be substituted away before much else happens. Yet, when I saw a skolem appear in a similar position after modifying the type-checker, I was sure I had done something wrong somewhere.
</p>
<p>
So, is this intended or accidental behavior? If accidental, should we be scared? If we needn't be scared, I'm happy to close this as wontfix, but a Note would probably be helpful somewhere. Apologies if that Note is already written and I missed it!
</p>
<p>
The same behavior is present in 7.8.1 RC 2 and in HEAD.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8907#changelog
http://ghc.haskell.org/trac/ghc/ticket/8808
http://ghc.haskell.org/trac/ghc/ticket/8808#8808: ImpredicativeTypes type checking fails depending on syntax of argumentsThu, 20 Feb 2014 05:40:52 GMTguest<p>
g1 and g2 below type check, but g1', g2', and g2<em> don't even though the types are exactly the same.
</em></p>
<pre class="wiki">{-# LANGUAGE ImpredicativeTypes, NoMonomorphismRestriction #-}
module Test where
f1 :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char])
f1 (Just g) = Just (g [3], g "hello")
f1 Nothing = Nothing
f2 :: [forall a. [a] -> [a]] -> Maybe ([Int], [Char])
f2 [g] = Just (g [3], g "hello")
f2 [] = Nothing
g1 = (f1 . Just) reverse
g1' = f1 (Just reverse)
g2 = f2 [reverse]
g2' = f2 ((:[]) reverse)
g2'' = f2 (reverse : [])
</pre><p>
Compiling it with HEAD gives these errors:
</p>
<pre class="wiki">[1 of 1] Compiling Test ( test.hs, test.o )
test.hs:12:16:
Couldn't match expected type ‛forall a. [a] -> [a]’
with actual type ‛[a2] -> [a2]’
In the first argument of ‛Just’, namely ‛reverse’
In the first argument of ‛f1’, namely ‛(Just reverse)’
test.hs:15:17:
Couldn't match expected type ‛forall a. [a] -> [a]’
with actual type ‛[a0] -> [a0]’
In the first argument of ‛: []’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛((: []) reverse)’
test.hs:16:12:
Couldn't match expected type ‛forall a. [a] -> [a]’
with actual type ‛[a1] -> [a1]’
In the first argument of ‛(:)’, namely ‛reverse’
In the first argument of ‛f2’, namely ‛(reverse : [])’
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/8808#changelog
http://ghc.haskell.org/trac/ghc/ticket/8799
http://ghc.haskell.org/trac/ghc/ticket/8799#8799: Orientation of given `Coercible` constraintsTue, 18 Feb 2014 17:22:33 GMTnomeata<pre class="wiki">Prelude> :m + GHC.Exts
Prelude GHC.Exts> let f :: Coercible a b => b -> a ; f = coerce
<interactive>:3:40:
Could not coerce from ‛b’ to ‛a’
because ‛b’ and ‛a’ are different types.
arising from a use of ‛coerce’
from the context (Coercible a b)
bound by the type signature for f :: Coercible a b => b -> a
at <interactive>:3:10-32
In the expression: coerce
In an equation for ‛f’: f = coerce
</pre><p>
Something better could be done here (but its not clear what exactly, and to what general extend).
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8799#changelog
http://ghc.haskell.org/trac/ghc/ticket/8779
http://ghc.haskell.org/trac/ghc/ticket/8779#8779: Exhaustiveness checks for pattern synonymsThu, 13 Feb 2014 09:40:51 GMTnomeata<p>
Pattern synonyms are great, as they decouple interface from implementation. Especially if <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/8581" title="feature request: Add support for explicitly-bidirectional pattern synonyms (new)">#8581</a> is also implemented, it should be possible to change a type completely while retaining the existing interface. Exciting!
</p>
<p>
Another missing piece is exhaustiveness checks. Given this pattern
</p>
<pre class="wiki">initLast [] = Nothing
initLast xs = Just (init xs, last xs)
pattern xs ::: x <- (initLast -> Just (xs,x))
</pre><p>
we want the compiler to tell the programmer that
</p>
<pre class="wiki">f [] = ...
f (xs ::: x) = ...
</pre><p>
is complete, while
</p>
<pre class="wiki">g (xs ::: x) = ...
</pre><p>
is not.
</p>
<p>
With view pattern directly, this is impossible. But the programmer did not write view patterns!
</p>
<p>
So here is what I think might work well, inspired by the new <tt>MINIMAL</tt> pragma:
</p>
<p>
We add a new pragma <tt>COMPLETE_PATTERNS</tt> (any ideas for a shorter name). The syntax is essentially the same as for <tt>MINIMAL</tt>, i.e. a boolean formula, with constructors and pattern synonyms as atoms. In this case.
</p>
<pre class="wiki">{-# COMPLETE_PATTERNS [] && (:::) #-}
</pre><p>
Multiple pragmas are obviously combined with <tt>||</tt>, and there is an implicit <tt>{-# COMPLETE_PATTERNS [] && (:) #-}</tt> listing all real data constructors.
</p>
<p>
When checking for exhaustiveness, this would be done before unfolding view patterns, and for <tt>g</tt> above we get a warning that <tt>[]</tt> is not matched. Again, the implementation is very much analogous to <tt>MINIMAL</tt>.
</p>
<p>
Clearly, a library author can mess up and give wrong <tt>COMPLETE_PATTERNS</tt> pragmas. I think that is ok (like with <tt>MINIMAL</tt>), and generally an improvement.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8779#changelog
http://ghc.haskell.org/trac/ghc/ticket/8778
http://ghc.haskell.org/trac/ghc/ticket/8778#8778: Typeable TypeNatsThu, 13 Feb 2014 08:13:59 GMTdmcclean<p>
It would be useful (the case I have at hand is for some scenarios involving checking of physical dimensions) to be able to combine the Data.Dynamic story with the GHC.<a class="missing wiki">TypeLits?</a> story.
</p>
<p>
A Typeable instance for every Nat is the sticking point.
</p>
<p>
(I do not know if this is even theoretically possible.)
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8778#changelog
http://ghc.haskell.org/trac/ghc/ticket/8672
http://ghc.haskell.org/trac/ghc/ticket/8672#8672: :browse and roles on typefamiliesThu, 16 Jan 2014 23:07:07 GMTmonoidal<p>
:browse on <tt>ghci tests/ghci.debugger/scripts/T8557.hs</tt> outputs a weird looking line:
</p>
<pre class="wiki">type role Sing nominal
data family Sing (a :: k)
type role T8557.R:Sing[]a nominal <--
data instance Sing a = SNil
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/8672#changelog
http://ghc.haskell.org/trac/ghc/ticket/8572
http://ghc.haskell.org/trac/ghc/ticket/8572#8572: Building an empty module with profiling requires profiling libraries for integer-gmpThu, 28 Nov 2013 19:06:30 GMTparcs<div class="code"><pre><span class="cm">{-# LANGUAGE NoImplicitPrelude #-}</span>
<span class="kr">module</span> <span class="nn">A</span> <span class="kr">where</span>
</pre></div><pre class="wiki">$ ghc-stage2 -prof -c A.hs
Top level:
Failed to load interface for ‛GHC.Integer.Type’
Perhaps you haven't installed the profiling libraries for package ‛integer-gmp’?
Use -v to see a list of the files searched for.
</pre><p>
I can't built module <tt>A</tt> without profiling libraries for <tt>integer-gmp</tt>, even though I don't use <tt>integer-gmp</tt> anywhere in the module.
</p>
<p>
This happens because the <tt>Tidy Core</tt> pass attempts to look up the <tt>mkInteger</tt> name (in order to desugar integer literals) even when there are no integer literals in the module.
</p>
<p>
The obvious fix is to lazily look up <tt>mkInteger</tt> in <tt>Coreprep.lookupMkIntegerName</tt>:
</p>
<div xmlns="http://www.w3.org/1999/xhtml" class="diff">
<ul class="entries">
<li class="entry">
<h2>
<a>compiler/coreSyn/CorePrep.lhs</a>
</h2>
<pre>diff --git a/compiler/coreSyn/CorePrep.lhs b/compiler/coreSyn/CorePrep.lhs
index 5e0cd65..9836982 100644</pre>
<table class="trac-diff inline" summary="Differences" cellspacing="0">
<colgroup><col class="lineno" /><col class="lineno" /><col class="content" /></colgroup>
<thead>
<tr>
<th title="File a/compiler/coreSyn/CorePrep.lhs">
a
</th>
<th title="File b/compiler/coreSyn/CorePrep.lhs">
b
</th>
<td><em> import Config</em> </td>
</tr>
</thead>
<tbody class="unmod">
<tr>
<th>56</th><th>56</th><td class="l"><span>import Data.Bits</span> </td>
</tr><tr>
<th>57</th><th>57</th><td class="l"><span>import Data.List ( mapAccumL )</span> </td>
</tr><tr>
<th>58</th><th>58</th><td class="l"><span>import Control.Monad</span> </td>
</tr>
</tbody><tbody class="add">
<tr class="last first">
<th> </th><th>59</th><td class="r"><ins>import System.IO.Unsafe ( unsafeInterleaveIO )</ins> </td>
</tr>
</tbody><tbody class="unmod">
<tr>
<th>59</th><th>60</th><td class="l"><span>\end{code}</span> </td>
</tr><tr>
<th>60</th><th>61</th><td class="l"><span></span> </td>
</tr><tr>
<th>61</th><th>62</th><td class="l"><span>-- ---------------------------------------------------------------------------</span> </td>
</tr>
</tbody>
<tbody class="skipped">
<tr>
<th><a href="#L1119">…</a></th>
<th><a href="#L1120">…</a></th>
<td><em> lookupMkIntegerName dflags hsc_env</em> </td>
</tr>
</tbody>
<tbody class="unmod">
<tr>
<th>1119</th><th>1120</th><td class="l"><span> else if thisPackage dflags == integerPackageId</span> </td>
</tr><tr>
<th>1120</th><th>1121</th><td class="l"><span> then return $ panic "Can't use Integer in integer"</span> </td>
</tr><tr>
<th>1121</th><th>1122</th><td class="l"><span> else liftM tyThingId</span> </td>
</tr>
</tbody><tbody class="add">
<tr class="last first">
<th> </th><th>1123</th><td class="r"><ins> $ unsafeInterleaveIO</ins> </td>
</tr>
</tbody><tbody class="unmod">
<tr>
<th>1122</th><th>1124</th><td class="l"><span> $ initTcForLookup hsc_env (tcLookupGlobal mkIntegerName)</span> </td>
</tr><tr>
<th>1123</th><th>1125</th><td class="l"><span></span> </td>
</tr><tr>
<th>1124</th><th>1126</th><td class="l"><span>mkInitialCorePrepEnv :: DynFlags -> HscEnv -> IO CorePrepEnv</span> </td>
</tr>
</tbody>
</table>
</li>
</ul>
</div><p>
This way, we don't attempt to look up <tt>mkInteger</tt> until we actually need it, i.e. if there are integer literals that we must desugar.
</p>
<p>
Relevant commits are <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/2ef5cd26db27543ac8664a3d18f45550d0109a8b/ghc" title="Put the Integer type, rather than the mkIntegerId, inside LitInteger
This ...">2ef5cd26db27543ac8664a3d18f45550d0109a8b</a> and <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/fdd552e0ecaa17300670a48562995040e1d6687e/ghc" title="Fix a build problem with integer-simple
We were trying to look up the ...">fdd552e0ecaa17300670a48562995040e1d6687e</a>
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8572#changelog
http://ghc.haskell.org/trac/ghc/ticket/8555
http://ghc.haskell.org/trac/ghc/ticket/8555#8555: Simplify given `Coercible` constraintsFri, 22 Nov 2013 14:00:56 GMTnomeata<p>
It would be feasible and possibly useful if
</p>
<pre class="wiki">foo :: Coercible [a] [b] => a -> b
foo = coerce
</pre><p>
would work. This involve simplifying <tt>CtGiven</tt>s similar to how given (nominal) equalities are simplified.
</p>
<p>
I’ll defer working on this, as it is not strictly required, it seems.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8555#changelog
http://ghc.haskell.org/trac/ghc/ticket/8550
http://ghc.haskell.org/trac/ghc/ticket/8550#8550: GHC builds recursive coerctions when using recursive type familiesThu, 21 Nov 2013 12:21:46 GMTnomeata<p>
Consider
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, GADTs, UndecidableInstances #-}
type family F a
type instance F () = F ()
data A where
A :: F () ~ () => A
x :: A
x = A
</pre><p>
On GHC 7.6.3 it yields a context reduction stack overflow (despite F () ~ () being put into the “solved funeqs” list).
</p>
<p>
In HEAD, a recursive dictionary is built, but then detected:
</p>
<pre class="wiki">[1 of 1] Compiling Foo ( Foo.hs, Foo.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 7.7.20131108 for x86_64-unknown-linux):
Cycle in coercion bindings
[[cobox_ayX{v} [lid]
= CO main:Foo.TFCo:R:F(){tc rob}[0] ; cobox_ayZ{v} [lid],
cobox_ayZ{v} [lid] = CO cobox_ayX{v} [lid] ; cobox_az0{v} [lid]]]
Please report this as a GHC bug: http://www.haskell.org/ghc/reportabug
</pre><p>
Either this panic needs to be turned into an error, or we need to prevent recursive dictionaries for when solving funeqs (similar to how we do it for <tt>Coercible</tt>).
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8550#changelog
http://ghc.haskell.org/trac/ghc/ticket/8516
http://ghc.haskell.org/trac/ghc/ticket/8516#8516: Add (->) representation and the Invariant class to GHC.GenericsSat, 09 Nov 2013 20:39:41 GMTnfrisby<p>
We currently disallow any use of the parameter in the domain of (->).
</p>
<pre class="wiki">newtype F a = F ((a -> Int) -> Int) deriving Generic1
<interactive>:4:38:
Can't make a derived instance of `Generic1 (F g)':
Constructor `F' must use the last type parameter only as the last argument of a data type, newtype, or (->)
In the data declaration for `F'
</pre><p>
DeriveFunctor succeeds for this F.
</p>
<p>
I'd like to add this representation type to GHC.Generics and DeriveGeneric.
</p>
<pre class="wiki">newtype (f :->: g) a = FArrow1 (f a -> g a)
</pre><p>
We could then represent the first example above. We could also derive the more interesting Generic1 (F g).
</p>
<pre class="wiki">newtype F g a = F (g a -> Int) deriving Generic1
type instance Rep1 (F g) = Rec1 g :->: Rec0 Int
instance Generic1 (F g) where
to x = F $ unRec0 . unArrow1 x . Rec1
from (F x) = FArrow1 $ Rec0 . x . unRec1
</pre><p>
Admittedly, there's not many generic definitions impeded by not having (:->:). Contra- and in-variant types are uncommon.
</p>
<p>
I'm suggesting this feature without strong motivating examples because I think this would streamline the implementation of -XDeriveGenerics in some ways while also making it more general — assuming that we added the Invariant class to base or ghc-prim.
</p>
<pre class="wiki">class Invariant t where
invmap :: (a -> b) -> (b -> a) -> t a -> t b
invmap_covariant :: Functor t => (a -> b) -> (b -> a) -> t a -> t b
invmap_covariant f _ = fmap f
instance (Invariant f,Invariant g) => Invariant (FArrow f g) where
invmap co contra (FArrow h) = FArrow $ invmap co contra . h . invmap contra co
</pre><p>
(Of course, Invariant should be a super class of Functor. :/ )
</p>
<p>
Now we can handle quite involved examples:
</p>
<pre class="wiki">newtype F g h a = F (g (h a)) deriving Generic1
instance Invariant g => Generic1 (F g h) where
to x = invmap unRec1 Rec1 $ unComp1 x
from (F x) = Comp1 $ invmap Rec1 unRec1
</pre><p>
All of that said, I'm mostly opening this ticket so I can get feedback on difficulties I might not be anticipating and have a place to reference from the compiler source code comments.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8516#changelog
http://ghc.haskell.org/trac/ghc/ticket/8447
http://ghc.haskell.org/trac/ghc/ticket/8447#8447: A combination of type-level comparison and subtraction does not work for 0Tue, 15 Oct 2013 06:19:42 GMTnushio<p>
The following function on type level naturals
</p>
<pre class="wiki"> Diff x y = If (x <=? y) (y-x) (x-y)
</pre><p>
does not work when either x or y is 0.
</p>
<p>
<a class="ext-link" href="https://github.com/nushio3/practice/blob/ea8a1716b1d6221ce32d77432b6de3f38e653a27/type-nats/int-bug.hs"><span class="icon"></span>https://github.com/nushio3/practice/blob/ea8a1716b1d6221ce32d77432b6de3f38e653a27/type-nats/int-bug.hs</a>
</p>
<p>
I've tested this code on ghc 7.7.20130926 since I couldn't build the really latest ghc. I'm sorry if it is already fixed on the ghc head.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8447#changelog
http://ghc.haskell.org/trac/ghc/ticket/8423
http://ghc.haskell.org/trac/ghc/ticket/8423#8423: contraint solver doesn't reduce reducible closed type family expressions (even with undecidable instances!)Tue, 08 Oct 2013 22:00:55 GMTcarter<p>
attached is an example where the type checker isn't "computing" in the closed type families, or at least doing a one step reduction.
</p>
<p>
this makes sense, given that type families only compute when instantiated...
But if we could partially evaluate closed type families (or at least do a one step reduction), the attached example code would type check!
</p>
<p>
interestingly, depending on what order the cases for the PSum are written, the type error changes!
</p>
<p>
I guess I want an "eager matching" closed type family, that when partially instantiated will patch on the first pattern it satisfies, to complement ordered type families.
</p>
<p>
attached is a toy example where I otherwise need an unsafeCoerce to make things type check
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8423#changelog
http://ghc.haskell.org/trac/ghc/ticket/8422
http://ghc.haskell.org/trac/ghc/ticket/8422#8422: type nats solver is too weak!Tue, 08 Oct 2013 21:02:58 GMTcarter<p>
I just built ghc HEAD today, and the type nat solver can't handle the attached program, which *should* be simple to check! (and while I could use unsafeCoerce to "prove" it correct, that defeats the purpose of having the type nat solver!)
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8422#changelog
http://ghc.haskell.org/trac/ghc/ticket/8161
http://ghc.haskell.org/trac/ghc/ticket/8161#8161: Associated type parameters that are more specific than the instance headerFri, 23 Aug 2013 12:45:59 GMTadamgundry<p>
It would be nice if type parameters of associated types could be more specific than those in the instance header. This is currently rejected with the message "Type indexes must match class instance head", but could be accepted:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
class C a where
type T a
instance C [a] where
type T [Bool] = Int
type T [Int] = Int
</pre><p>
More typically, this is useful where we want to use an equality constraint to make type inference easier, but need to match on the actual type in an associated type:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
class C a where
type T a
instance a ~ [b] => C a where
type T [b] = Int
</pre><p>
This showed up in the implementation of <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/Plan">OverloadedRecordFields</a>. Of course, one can always work around it using a normal (non-associated) type family.
</p>
<p>
Note that we already allow type families to specialise variables that do not occur in the instance header:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
class C a where
type T a b
instance C [a] where
type T [a] [Bool] = Bool
type T [a] [Int] = Int
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/8161#changelog
http://ghc.haskell.org/trac/ghc/ticket/8128
http://ghc.haskell.org/trac/ghc/ticket/8128#8128: Standalone deriving fails for GADTs due to inaccessible codeTue, 13 Aug 2013 09:56:20 GMTadamgundry<p>
Consider the following:
</p>
<pre class="wiki">{-# LANGUAGE StandaloneDeriving, GADTs, FlexibleInstances #-}
module StandaloneDerivingGADT where
data T a where
MkT1 :: T Int
MkT2 :: (Bool -> Bool) -> T Bool
deriving instance Show (T Int)
</pre><p>
This gives the error:
</p>
<pre class="wiki">StandaloneDerivingGADT.hs:9:1:
Couldn't match type ‛Int’ with ‛Bool’
Inaccessible code in
a pattern with constructor
MkT2 :: (Bool -> Bool) -> T Bool,
in an equation for ‛showsPrec’
In the pattern: MkT2 b1
In an equation for ‛showsPrec’:
showsPrec a (MkT2 b1)
= showParen
((a >= 11)) ((.) (showString "MkT2 ") (showsPrec 11 b1))
When typechecking the code for ‛showsPrec’
in a standalone derived instance for ‛Show (T Int)’:
To see the code I am typechecking, use -ddump-deriv
In the instance declaration for ‛Show (T Int)’
</pre><p>
The derived instance declaration matches on all the constructors, even if they cannot possibly match. It should omit obviously inaccessible constructors so that this example is accepted. For reference, the derived code is:
</p>
<pre class="wiki"> instance GHC.Show.Show
(StandaloneDerivingGADT.T GHC.Types.Int) where
GHC.Show.showsPrec _ StandaloneDerivingGADT.MkT1
= GHC.Show.showString "MkT1"
GHC.Show.showsPrec a_aij (StandaloneDerivingGADT.MkT2 b1_aik)
= GHC.Show.showParen
((a_aij GHC.Classes.>= 11))
((GHC.Base..)
(GHC.Show.showString "MkT2 ") (GHC.Show.showsPrec 11 b1_aik))
GHC.Show.showList = GHC.Show.showList__ (GHC.Show.showsPrec 0)
</pre><p>
The same problem applies to other derivable classes (e.g. <tt>Eq</tt>).
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8128#changelog
http://ghc.haskell.org/trac/ghc/ticket/8095
http://ghc.haskell.org/trac/ghc/ticket/8095#8095: TypeFamilies painfully slowSat, 27 Jul 2013 02:54:34 GMTMikeIzbicki<p>
I'm using the <a class="missing wiki">TypeFamilies?</a> extension to generate types that are quite large. GHC can handle these large types fine when they are created manually, but when type families get involved, GHC's performance dies.
</p>
<p>
Unlike in ticket <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/5321" title="bug: Very slow constraint solving for type families (closed: fixed)">#5321</a>, using tail recursion does not eliminate the problem, and the order of arguments greatly affects compile time.
</p>
<p>
I've attached a file Types.hs that demonstrates the problems. This file generates another Haskell file which has the problems. It takes 3 flags. The first is the size of the type to generate, the second is which type family function to use, and the third is whether to call the type family or just use a manually generated type.
</p>
<p>
Here are my performance results:
</p>
<p>
Using non-tail recursion, I get these results. I have to increase the stack size based on the size of the type I want to generate.
</p>
<pre class="wiki">$ ./Types 200 a a > test.hs && time ghc test.hs > /dev/null -fcontext-stack=250
real 0m2.973s
$ ./Types 300 a a > test.hs && time ghc test.hs > /dev/null -fcontext-stack=350
real 0m6.018s
$ ./Types 400 a a > test.hs && time ghc test.hs > /dev/null -fcontext-stack=450
real 0m9.995s
$ ./Types 500 a a > test.hs && time ghc test.hs > /dev/null -fcontext-stack=550
real 0m15.645s
</pre><p>
Tail recursion generates much slower compile times for some reason, and I still need to adjust the stack size:
</p>
<pre class="wiki">$ ./Types 200 b a > test.hs && time ghc test.hs > /dev/null -fcontext-stack=250
real 0m16.120s
</pre><p>
Changing the order of arguments to the recursive type family greatly changes the run times:
</p>
<pre class="wiki">$ ./Types 200 c a > test.hs && time ghc test.hs > /dev/null -fcontext-stack=250
real 0m6.095s
</pre><p>
Without the type family, I get MUCH better performance:
</p>
<pre class="wiki">$ ./Types 10000 a d > test.hs && time ghc test.hs > /dev/null
real 0m2.271s
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/8095#changelog
http://ghc.haskell.org/trac/ghc/ticket/8044
http://ghc.haskell.org/trac/ghc/ticket/8044#8044: "Inaccessible code" error reported in wrong placeMon, 08 Jul 2013 08:57:24 GMTgoldfire<p>
Here is my file <tt>Bug.hs</tt>:
</p>
<pre class="wiki">{-# LANGUAGE GADTs, TypeFamilies #-}
module Bug where
data X a where
XInt :: X Int
XBool :: X Bool
XChar :: X Char
type family Frob a where
Frob Int = Int
Frob x = Char
frob :: X a -> X (Frob a)
frob XInt = XInt
frob _ = XChar
</pre><p>
Compiling this file produces the error
</p>
<pre class="wiki">Bug.hs:15:6:
Couldn't match type ‛Int’ with ‛Char’
Inaccessible code in
a pattern with constructor XInt :: X Int, in an equation for ‛frob’
In the pattern: XInt
In an equation for ‛frob’: frob XInt = XInt
</pre><p>
The line/column number single out the pattern <tt>XInt</tt> in the first clause of the function <tt>frob</tt>. But, the real problem (as I see it), is the right-hand side of the <em>second</em> clause of <tt>frob</tt>. Indeed, when I comment out the second line of the function, the error goes away, even though it was reported on the first line.
</p>
<p>
I do not believe that this error is caused by closed type families, per se, because I have run across it without them, just in code that was too hard to pare down enough to make a bug report out of.
</p>
<p>
This was tested on 7.7.20130702.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8044#changelog
http://ghc.haskell.org/trac/ghc/ticket/8025
http://ghc.haskell.org/trac/ghc/ticket/8025#8025: "During interactive linking, GHCi couldn't find the following symbol" typechecker error with TemplateHaskell involvedSun, 30 Jun 2013 19:43:53 GMTmojojojo<p>
Building the included project with
</p>
<pre class="wiki">cabal configure && cabal build --ghc-options="-fforce-recomp -Wall -fno-code"
</pre><p>
results in the following typechecker error:
</p>
<pre class="wiki">ByteCodeLink.lookupCE
During interactive linking, GHCi couldn't find the following symbol:
supabugzm0zi1zi0_A_makeLenseszq_closure
This may be due to you not asking GHCi to load extra object files,
archives or DLLs needed by your current session. Restart GHCi, specifying
the missing library using the -L/path/to/object/dir and -lmissinglibname
flags, or simply by naming the relevant files on the GHCi command line.
Alternatively, this link failure might indicate a bug in GHCi.
If you suspect the latter, please send a bug report to:
glasgow-haskell-bugs@haskell.org
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/8025#changelog
http://ghc.haskell.org/trac/ghc/ticket/7870
http://ghc.haskell.org/trac/ghc/ticket/7870#7870: Compilation errors break the complexity encapsulation on DSLs, impairs success in industrySat, 27 Apr 2013 08:59:03 GMTagocorona<p>
From the paper "Scripting the Type Inference Process" -Bastiaan Heeren Jurriaan Hage S. Doaitse Swierstra:
</p>
<p>
... Combinator languages are a means of deﬁning domain speciﬁc languages embedded within an existing programming language, using the abstraction facilities present in the latter. However, since the domain speciﬁc extensions are mapped to constructs present in the underlying language, all type errors are reported in terms of the host language, and not in terms of concepts from the combinator library. In addition, the developer of a combinator library may be aware of various mistakes which users of the library can make, something which he can explain in the documentation for the library, but which he cannot make part of the library itself.
</p>
<p>
...As a result, the beginning programmer is likely to be discouraged from pro-gramming in a functional language, and may see the rejection of programs as a nuisance instead of a blessing. The experienced user might not look at the messages at all.
</p>
<p>
Definitively this is probably the biggest barrier for the acceptance of Haskell on Industry. We need to start with something not as sophisticated as the Helium paper "Scripting the Type Inference Process", but maybe a partial implementation of the techniques mentioned, so that the development can be enhanced in the future.
</p>
<p>
Maybe some kind of library that permits postprocessing of GHC errors and/or the identification of points in the current type checker where some kind of rules can be defined by the programmer can be the first step.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7870#changelog
http://ghc.haskell.org/trac/ghc/ticket/7862
http://ghc.haskell.org/trac/ghc/ticket/7862#7862: Could not deduce (A) from the context (A, ...)Thu, 25 Apr 2013 07:56:46 GMTalang9<p>
The following code doesn't compile and produces a strange error:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
module Numeric.AD.Internal.Tower () where
type family Scalar t
newtype Tower s a = Tower [a]
type instance Scalar (Tower s a) = a
class (Num (Scalar t), Num t) => Mode t where
(<+>) :: t -> t -> t
instance (Num a) => Mode (Tower s a) where
Tower as <+> _ = undefined
where
_ = (Tower as) <+> (Tower as)
instance Num a => Num (Tower s a) where
</pre><pre class="wiki">src/Numeric/AD/Internal/Tower.hs:17:24:
Could not deduce (Num (Scalar (Tower s a)))
arising from a use of `<+>'
from the context (Num (Scalar (Tower s a)), Num (Tower s a), Num a)
bound by the instance declaration
at src/Numeric/AD/Internal/Tower.hs:14:10-36
Possible fix:
add an instance declaration for (Num (Scalar (Tower s a)))
In the expression: (Tower as) <+> (Tower as)
In a pattern binding: _ = (Tower as) <+> (Tower as)
In an equation for `<+>':
(Tower as) <+> _
= undefined
where
_ = (Tower as) <+> (Tower as)
</pre><p>
Furthermore, Removing the <tt>Num (Scalar t)</tt> constraint from the <tt>Mode</tt> class produces a different strange error:
</p>
<pre class="wiki">src/Numeric/AD/Internal/Tower.hs:17:24:
Overlapping instances for Num (Tower s0 a)
arising from a use of `<+>'
Matching givens (or their superclasses):
(Num (Tower s a))
bound by the instance declaration
at src/Numeric/AD/Internal/Tower.hs:14:10-36
Matching instances:
instance Num a => Num (Tower s a)
-- Defined at src/Numeric/AD/Internal/Tower.hs:19:10
(The choice depends on the instantiation of `a, s0')
In the expression: (Tower as) <+> (Tower as)
In a pattern binding: _ = (Tower as) <+> (Tower as)
In an equation for `<+>':
(Tower as) <+> _
= undefined
where
_ = (Tower as) <+> (Tower as)
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/7862#changelog
http://ghc.haskell.org/trac/ghc/ticket/7849
http://ghc.haskell.org/trac/ghc/ticket/7849#7849: Error on pattern matching of an existential whose context includes a type functionSat, 20 Apr 2013 04:41:26 GMTguest<p>
The following code
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
module Ex where
import Data.IORef
class SUBJ subj where
type SUBJ_Obs subj :: *
unsubscribe' :: subj -> SUBJ_Obs subj -> IO ()
data ASubj obs = forall subj. (SUBJ subj, SUBJ_Obs subj ~ obs) => ASubj subj
-- data ASubj obs = forall subj. (SUBJ subj) => ASubj subj (obs -> SUBJ_Obs subj)
class OBS obs where
subscribed :: obs -> ASubj obs -> IO ()
withdraw :: obs -> IO ()
-- The implementation of Obs
data Obs = Obs{obs_subjects :: IORef [ASubj Obs]}
instance OBS Obs where
subscribed obs subj = modifyIORef (obs_subjects obs) (subj:)
withdraw obs = do
subjs <- readIORef (obs_subjects obs)
writeIORef (obs_subjects obs) []
mapM_ (\ (ASubj subj) -> unsubscribe' subj obs) subjs
-- mapM_ (\ (ASubj subj cast) -> unsubscribe' subj (cast obs)) subjs
</pre><p>
gives a rather obscure type error
</p>
<pre class="wiki"> Couldn't match type `b0' with `()'
`b0' is untouchable
inside the constraints (SUBJ subj, SUBJ_Obs subj ~ Obs)
bound at a pattern with constructor
ASubj :: forall obs subj.
(SUBJ subj, SUBJ_Obs subj ~ obs) =>
subj -> ASubj obs,
in a lambda abstraction
In the pattern: ASubj subj
In the first argument of `mapM_', namely
`(\ (ASubj subj) -> unsubscribe' subj obs)'
In a stmt of a 'do' block:
mapM_ (\ (ASubj subj) -> unsubscribe' subj obs) subjs
-}
</pre><p>
It is not even clear what b0 is: the code has no type variable named b.
Incidentally, if I use the explicit cast (as in the commented out
declaration of ASubj) and change the last line of withdraw accordingly (as shown in the commented out line), the code compiles.
It seems that what I am trying to accomplish is reasonable.
</p>
<p>
Incidentally, why GHC insists on the extension GADTs given that I already specified <a class="missing wiki">ExistentialQuantification?</a>? It seems when opening amn existential GADTs extension must be present. It seems <a class="missing wiki">ExistentialQuantification?</a> no longer has any point?
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7849#changelog
http://ghc.haskell.org/trac/ghc/ticket/7842
http://ghc.haskell.org/trac/ghc/ticket/7842#7842: Incorrect checking of let-bindings in recursive doWed, 17 Apr 2013 00:00:50 GMTdiatchki<p>
I have run into a problem with the type-checking of recursive do blocks, which reduces to the following example:
</p>
<pre class="wiki">{-# LANGUAGE RecursiveDo #-}
module Bug where
bug :: (Int -> IO Int) -> IO (Bool, Char)
bug m =
mdo i <- m i1 -- RECURSION
let i1 :: Int
i1 = i -- RECURSION
-- This appears to be monomorphic, despite the type signature.
f :: b -> b
f x = x
return (f True, f 'a')
</pre><p>
This program is rejected with the errors shown below. The problem appears to be that somehow <tt>f</tt> has become monomorphic, despite its type-signature. This seems to happen only when <tt>f</tt> is part of a <tt>let</tt> block that is also involved in the recursion.
</p>
<p>
Here is the error reported by GHC 7.7.20130215:
</p>
<pre class="wiki">Bug.hs:15:23:
Couldn't match expected type `Char' with actual type `Bool'
In the return type of a call of `f'
In the expression: f 'a'
In the first argument of `return', namely `(f True, f 'a')'
Bug.hs:15:25:
Couldn't match expected type `Bool' with actual type `Char'
In the first argument of `f', namely 'a'
In the expression: f 'a'
In the first argument of `return', namely `(f True, f 'a')'
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/7842#changelog
http://ghc.haskell.org/trac/ghc/ticket/7828
http://ghc.haskell.org/trac/ghc/ticket/7828#7828: RebindableSyntax and ArrowWed, 10 Apr 2013 14:49:38 GMTAlessandroVermeulen<p>
When trying to add constraints to the types of the arrow primitives I get a type error. I think that doing such a thing should be possible and I've attached the code I used to test this. The errors I get when using the arrow notation for the function test are as follows:
</p>
<pre class="wiki">test :: Typeable a => R a a
test = proc n -> returnA -< n
</pre><pre class="wiki">bug-arrow.hs:15:8:
Could not deduce (Typeable c) arising from a use of `arr'
from the context (Typeable a)
bound by the type signature for test :: Typeable a => R a a
at bug-arrow.hs:14:9-27
Possible fix:
add (Typeable c) to the context of
a type expected by the context: (b -> c) -> R b c
or the type signature for test :: Typeable a => R a a
In the expression: arr
When checking that `arr' (needed by a syntactic construct)
has the required type: forall b1 c1. (b1 -> c1) -> R b1 c1
arising from a proc expression at bug-arrow.hs:15:8-29
In the expression: proc n -> returnA -< n
bug-arrow.hs:15:8:
Could not deduce (Typeable c) arising from a use of `>>>'
from the context (Typeable a)
bound by the type signature for test :: Typeable a => R a a
at bug-arrow.hs:14:9-27
Possible fix:
add (Typeable c) to the context of
a type expected by the context: R a1 b -> R b c -> R a1 c
or the type signature for test :: Typeable a => R a a
In the expression: (>>>)
When checking that `(>>>)' (needed by a syntactic construct)
has the required type: forall a2 b1 c1.
R a2 b1 -> R b1 c1 -> R a2 c1
arising from a proc expression at bug-arrow.hs:15:8-29
In the expression: proc n -> returnA -< n
bug-arrow.hs:15:8:
Could not deduce (Typeable d) arising from a use of `first'
from the context (Typeable a)
bound by the type signature for test :: Typeable a => R a a
at bug-arrow.hs:14:9-27
Possible fix:
add (Typeable d) to the context of
a type expected by the context: R b c -> R (b, d) (c, d)
or the type signature for test :: Typeable a => R a a
In the expression: first
When checking that `first' (needed by a syntactic construct)
has the required type: forall b1 c1 d1.
R b1 c1 -> R (b1, d1) (c1, d1)
arising from a proc expression at bug-arrow.hs:15:8-29
In the expression: proc n -> returnA -< n
</pre><p>
When I replace the definition with the translated core code (minus type applications and scoped type variables) the code compiles:
</p>
<pre class="wiki">test :: Typeable a => R a a
test =
(>>>)
(arr (\ (n_apd) -> n_apd))
((>>>)
(arr (\ (ds_dst) -> ds_dst))
(returnA)
)
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/7828#changelog
http://ghc.haskell.org/trac/ghc/ticket/7788
http://ghc.haskell.org/trac/ghc/ticket/7788#7788: Recursive type family causes <<loop>>Sat, 23 Mar 2013 04:18:09 GMTshachaf<p>
This file:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
data Proxy a = Proxy
foo :: Proxy (F (Fix Id)) -> ()
foo = undefined
newtype Fix a = Fix (a (Fix a))
newtype Id a = Id a
type family F a
type instance F (Fix a) = F (a (Fix a))
type instance F (Id a) = F a
main :: IO ()
main = print $ foo Proxy
</pre><p>
Dies with <tt><<loop>></tt>. The type family is recursive, of course:
</p>
<pre class="wiki">*Main> :kind! F (Fix Id)
F (Fix Id) :: *^CInterrupted.
</pre><p>
But <tt><<loop>></tt> is still not the behavior I'd expect. The actual value is just <tt>undefined</tt>.
</p>
<p>
In the file that this example came up, the situation was even worse -- there was a situation where
</p>
<pre class="wiki">moldMapOf l f = runAccessor . l (Accessor . f)
main = print $ (flip appEndo [] . moldMapOf (ix 3) (Endo . (:)) $ testVal :: [Int]) -- <<loop>>
main = print $ (flip appEndo [] . runAccessor . (ix 3) (Accessor . Endo . (:)) $ testVal :: [Int]) -- undefined
</pre><p>
I.e. substitution can turn one program (which happens to be ⊥ here, admittedly, but that's not fundamental) into another (<tt><<loop>></tt>). This makes it very tricky to track down the recursive type family. If necessary I can hunt down a working test case and post it here -- it's a bit tricky to get working, though.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7788#changelog
http://ghc.haskell.org/trac/ghc/ticket/7730
http://ghc.haskell.org/trac/ghc/ticket/7730#7730: :info and polykindsFri, 01 Mar 2013 23:30:33 GMTmonoidal<pre class="wiki">ghci -XPolyKinds
Prelude> data A x y
Prelude> :i A
data A k k x y -- Defined at <interactive>:3:6
</pre><p>
The two <tt>k</tt> might be different. It should be either <tt>A k l x y</tt> or - without kind variables - <tt>A x y</tt>.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7730#changelog
http://ghc.haskell.org/trac/ghc/ticket/7672
http://ghc.haskell.org/trac/ghc/ticket/7672#7672: boot file entities are sometimes invisible and are not (semantically) unified with corresponding entities in implementing moduleThu, 07 Feb 2013 19:01:00 GMTskilpat<p>
In a recursive module (i.e. a module that transitively imports itself), the unique "Name" of an entity E declared in this module's boot file should be precisely the same as that of the corresponding E defined in the module. Right now GHC appears to treat them as separate entities. (In the module systems literature, this problem has been identified as the "double vision problem" [1, Ch 5] and in general has caused problems with implementations of recursive modules. Derek Dreyer and his coauthors have proposed a number of solutions <a class="missing changeset" title="No changeset 2 in the repository">[2]</a>, and so have Im et al. more recently in the context of OCaml <a class="missing changeset" title="No changeset 3 in the repository">[3]</a>.)
</p>
<p>
With that being said, the <em>immediate</em> problem here seems to be that GHC does not actually allow, in the implementing module, the import of its boot file's entities.
</p>
<p>
There are a couple related errors I can identify with, huzzah!, very small example programs. The crux of the example is that the module A defines a data type T which is essentially the typical Nat data type -- except that the recursive type reference in the successor constructor refers to the "forward declaration's" view of the type (in the boot file) rather than the local view of that data type T.
</p>
<p>
This first example shows that the boot file import is not actually making available the entities it declares:
</p>
<pre class="wiki">module A where
data T
</pre><pre class="wiki">module A where
import {-# SOURCE #-} qualified A as Decl(T)
data T = Z | S Decl.T
</pre><p>
The Decl.T reference should have the exact same identity as the locally defined T reference; after tying the module knot, this data type should be the same as if we had defined it with a T instead of Decl.T. However, the entity name T does not even appear to be gotten from the import of the boot file:
</p>
<pre class="wiki">A.hs:3:18: Not in scope: type constructor or class `Decl.T'
</pre><p>
In an earlier version of GHC I tested, 6.12.1, the error message lies on the import statement:
</p>
<pre class="wiki">A.hs:2:44: Module `A' (hi-boot interface) does not export `T'
</pre><p>
In the next example, with the same boot file, we see that the mechanism that checks whether the implementation matches the boot file fails to see the two "views" of T as the same. (Note that I changed the definition of T here to make the previous error go away.)
</p>
<pre class="wiki">module A(Decl.T(..)) where
import {-# SOURCE #-} qualified A as Decl(T)
data T = Z | S T
</pre><p>
Since Decl.T should point to the same entity as T, the export statement should have the same effect as if it were instead "(T(..))". However, GHC again cannot make sense of the reference "Decl.T" and then complains that the boot file's T is not provided in the implementation:
</p>
<pre class="wiki">A.hs:1:10: Not in scope: type constructor or class `Decl.T'
<no location info>:
T is exported by the hs-boot file, but not exported by the module
</pre><p>
(Making the export list empty shows this second error message only.)
</p>
<p>
Altering this second example by omitting the alias on the import, and by changing the T reference in the type's definition to A.T, results in a well-typed module:
</p>
<pre class="wiki">module A(A.T(..)) where
import {-# SOURCE #-} qualified A(T)
data T = Z | S A.T
</pre><p>
A final example shows that, in a module that is <em>not</em> the implementing module, entities defined in the boot file are imported as one would expect! In the following example, we insert a module B, in between A's boot file and A's implementation, which merely passes along the boot file's view of T.
</p>
<pre class="wiki">module A where
data T
</pre><pre class="wiki">module B(Decl.T(..)) where
import {-# SOURCE #-} qualified A as Decl(T)
data U = U Decl.T
</pre><pre class="wiki">module A(T(..)) where
import qualified B(T)
data T = Z | S B.T
</pre><p>
The error message here, again, lies in the reference B.T in A's implementation:
</p>
<pre class="wiki">A.hs:3:18:
Not in scope: type constructor or class `B.T'
Perhaps you meant `A.T' (line 3)
</pre><p>
Notice, however, that the reference to Decl.T in the B module is perfectly well-formed.
</p>
<p>
I suspect that the general problem lies with double vision, and that the more immediate problem--whereby imports of boot file entities from their implementing modules fail--is merely the manifestation of that.
</p>
<p>
In the above, wherever I have suggested an intended semantics, I refer primarily to the state of the art in recursive modules systems. A perhaps more pressing justification, however, is that both the Haskell language report and Diatchki et al.'s specification of the module system <a class="missing changeset" title="No changeset 4 in the repository">[4]</a> (seem to) corroborate that intended semantics.
</p>
<p>
Your friend in the recursive module swamp,<br />
Scott Kilpatrick
</p>
<hr />
<p>
References
</p>
<p>
<a class="missing changeset" title="No changeset 1 in the repository">[1]</a> Derek Dreyer. <em><a class="ext-link" href="http://www.mpi-sws.org/~dreyer/thesis/main.pdf"><span class="icon"></span>Understanding and Evolving the ML Module System</a></em>, PhD thesis, 2005.<br />
<a class="missing changeset" title="No changeset 2 in the repository">[2]</a> Derek Dreyer. <em><a class="ext-link" href="http://www.mpi-sws.org/~dreyer/courses/modules/dreyer07.pdf"><span class="icon"></span>A Type System for Recursive Modules</a></em>, ICFP 2007.<br />
<a class="missing changeset" title="No changeset 3 in the repository">[3]</a> Hyeonseung Im, Keiko Nakata, Jacques Garrigue, and Sungwoo Park. <em><a class="ext-link" href="http://dl.acm.org/citation.cfm?doid=2048066.2048141"><span class="icon"></span>A syntactic type system for recursive modules</a></em>, OOPSLA 2011.<br />
<a class="missing changeset" title="No changeset 4 in the repository">[4]</a> Iavor S. Diatchki, Mark P. Jones, and Thomas Hallgren. <em><a class="ext-link" href="http://web.cecs.pdx.edu/~mpj/pubs/hsmods.html"><span class="icon"></span>A formal specification of the Haskell 98 module system</a></em>, Haskell 2002.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7672#changelog
http://ghc.haskell.org/trac/ghc/ticket/7668
http://ghc.haskell.org/trac/ghc/ticket/7668#7668: Location in -fdefer-type-errorsWed, 06 Feb 2013 18:28:49 GMTmonoidal<p>
Consider
</p>
<pre class="wiki">x :: Char
x = 'x' + 1
y :: Char
y = 'y' + 1
</pre><p>
Run <tt>ghci -fdefer-type-errors</tt>:
</p>
<pre class="wiki">*Main> x
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equation for `y': y = 'y' + 1
(deferred type error)
*Main> y
*** Exception: G.hs:5:9:
No instance for (Num Char) arising from a use of `+'
In the expression: 'y' + 1
In an equation for `y': y = 'y' + 1
(deferred type error)
</pre><p>
The first exception is wrong. It seems that the missing <tt>Num Char</tt> instance is filled with the same error message in all places where the constraint should be supplied.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7668#changelog
http://ghc.haskell.org/trac/ghc/ticket/7643
http://ghc.haskell.org/trac/ghc/ticket/7643#7643: Kind application errorThu, 31 Jan 2013 13:55:01 GMTgmainland<p>
Compiling the attached program with -dcore-lint fails. This failure is a reduced version of code taken from the primitive package, version 0.5.0.1.
</p>
<p>
To see the failure:
</p>
<pre class="wiki">ghc -dcore-lint --make Main.hs
</pre><p>
The failure does not occur with GHC 7.4.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7643#changelog
http://ghc.haskell.org/trac/ghc/ticket/7503
http://ghc.haskell.org/trac/ghc/ticket/7503#7503: Bug with PolyKinds, type synonyms & GADTsSun, 16 Dec 2012 23:37:00 GMTAshley Yakeley<p>
GHC incorrectly rejects this program:
</p>
<pre class="wiki">{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #-}
module TestConstraintKinds where
import GHC.Exts hiding (Any)
data WrappedType = forall a. WrapType a
data A :: WrappedType -> * where
MkA :: forall (a :: *). AW a -> A (WrapType a)
type AW (a :: k) = A (WrapType a)
type AW' (a :: k) = A (WrapType a)
class C (a :: k) where
aw :: AW a -- workaround: AW'
instance C [] where
aw = aw
</pre><p>
GHC accepts the program when AW is replaced with AW' on that line.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7503#changelog
http://ghc.haskell.org/trac/ghc/ticket/7494
http://ghc.haskell.org/trac/ghc/ticket/7494#7494: Allow compatible type synonyms to be the return type of a GADT data constructor.Mon, 10 Dec 2012 15:23:32 GMTtopi<p>
Please consider adding support for something like:
</p>
<pre class="wiki">{-# LANGUAGE GADTs #-}
data Steps s y where
Yield :: y -> FK s y -> FK s y
Done :: Steps s y
newtype M y s a = M { unM :: (a -> FK s y) -> FK s y }
type FK s y = s -> Steps s y
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/7494#changelog
http://ghc.haskell.org/trac/ghc/ticket/7461
http://ghc.haskell.org/trac/ghc/ticket/7461#7461: Error messages about "do" statements contain false informationFri, 30 Nov 2012 00:49:08 GMTEyalLotem<p>
When GHC complains about a type-error in a "do" block, it says, for example:
</p>
<pre class="wiki">main = putChar $ do
getLine
return 'x'
</pre><p>
Results in an error:
</p>
<pre class="wiki"> Couldn't match type `IO Char' with `Char'
Expected type: IO String -> IO Char -> Char
Actual type: IO String -> IO Char -> IO Char
In a stmt of a 'do' block: getLine
</pre><p>
I think this error message is pretty directly saying: The <strong>Actual</strong> type of "getLine" is:
</p>
<pre class="wiki">IO String -> IO Char -> IO Char
</pre><p>
But that is of course non-sense! It is actually talking about the type of the (>>=) binding the "getLine" to the rest of the statements. But the (>>=) is not "in the statement" at all, so the error message is plainly wrong.
</p>
<p>
It would be much better to talk about the type of the entire do block, or maybe the type of the last stmt in the do block (which is the same).
</p>
<p>
For example, the error could be replaced by:
</p>
<pre class="wiki"> Couldn't match type `IO Char' with `Char'
Expected type: Char
Actual type: IO Char
In a stmt of a 'do' block: return 'x'
</pre><p>
Or by:
</p>
<pre class="wiki"> Couldn't match type `IO Char' with `Char'
Expected type: Char
Actual type: IO Char
In 'do' block: `do { getLine;
return 'x' }'
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/7461#changelog
http://ghc.haskell.org/trac/ghc/ticket/7296
http://ghc.haskell.org/trac/ghc/ticket/7296#7296: ghc-7 assumes incoherent instances without requiring language `IncoherentInstances`Thu, 04 Oct 2012 12:50:04 GMTmaeder<p>
the attached examples works with ghc-7 and returns
</p>
<pre class="wiki"> *Main> a
[Spec1 Spec2]
*Main> b
[]
</pre><p>
(One may wish that b also returned [Spec1 Spec2])
</p>
<p>
ghc-6 complains with
</p>
<pre class="wiki">Splittable.hs:16:36:
Overlapping instances for Test a Spec2
arising from a use of `test' at Splittable.hs:16:36-43
Matching instances:
instance [overlap ok] Test a Spec2
-- Defined at Splittable.hs:20:13-24
instance [overlap ok] Test Bool Spec2
-- Defined at Splittable.hs:25:13-27
(The choice depends on the instantiation of `a'
To pick the first instance above, use -XIncoherentInstances
when compiling the other instance declarations)
In the second argument of `($)', namely `test a b'
In the expression: map Spec1 $ test a b
In the definition of `test':
test a (Spec1 b) = map Spec1 $ test a b
Failed, modules loaded: none.
</pre><p>
After adding <tt>IncoherentInstances</tt> the file also goes through ghc-6 with the same results.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7296#changelog
http://ghc.haskell.org/trac/ghc/ticket/7140
http://ghc.haskell.org/trac/ghc/ticket/7140#7140: Allow type signature in export listMon, 13 Aug 2012 15:54:27 GMTdrb226<p>
In response to the new <a class="missing wiki">InstanceSigs?</a> extension in the 7.6.1 RC1, waterlight on Reddit suggested the following:
</p>
<p>
"While we're at it, why not also allow type signatures in export lists? People tend to add them anyway as comments, just because it's useful documentation. Checking for consistency would be nice."
</p>
<p>
The desired syntax, therefore, is something like this:
</p>
<pre class="wiki">{-# LANGUAGE ExportSigs #-}
module Foo
( foo :: Bar -> Baz
, Blah ( Blip :: a -> Blah a
, Bloop :: Blah Int )
, Quux ( quux :: Quux q => a -> q a
, qux :: Quux q => q (q ()) )
) where
...
</pre><p>
where all of the type annotations here are optional, and can be <strong>no less restrictive</strong> than the corresponding type signatures provided at the definition site, if provided (whether that be in that file's own code, or imported from another file).
</p>
<p>
This would have non-trivial interaction with -fno-warn-missing-signatures, and consequently, with <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/2526" title="feature request: warn about missing signatures only for exported functions (new)">#2526</a>.
There may also be non-trivial interaction with GADTs, if we allow exported constructors to be annotated with a type signature.
</p>
<p>
This idea was vaguely referenced by <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1404" title="feature request: allow more type signatures (new)">#1404</a>, to which igloo responded:
</p>
<p>
"Type sigs in export lists might be nice, as some people seem to like giving them as comments which then get out of sync with the actual types."
</p>
<p>
If we are to consider this sort of thing for Haskell', we should try it out as a GHC extension first.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7140#changelog
http://ghc.haskell.org/trac/ghc/ticket/7026
http://ghc.haskell.org/trac/ghc/ticket/7026#7026: Impredicative implicit parametersSat, 23 Jun 2012 17:36:30 GMTAshley Yakeley<p>
There doesn't seem to be a way to make impredicative implicit parameters work in 7.4.2:
</p>
<pre class="wiki">{-# LANGUAGE ImplicitParams, ImpredicativeTypes #-}
module Bug where
f1 :: Maybe ((?a :: Bool) => Char)
f1 = Just 'C'
f2 :: Maybe ((?a :: Bool) => Bool)
f2 = Just ?a
</pre><pre class="wiki">$ ghc -c Bug.hs
Bug.hs:5:15:
Couldn't match expected type `(?a::Bool) => Char'
with actual type `Char'
In the first argument of `Just', namely 'C'
In the expression: Just 'C'
In an equation for `f1': f1 = Just 'C'
Bug.hs:8:15:
Unbound implicit parameter (?a::(?a::Bool) => Bool)
arising from a use of implicit parameter `?a'
In the first argument of `Just', namely `?a'
In the expression: Just ?a
In an equation for `f2': f2 = Just ?a
</pre><p>
I believe this used to work?
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/7026#changelog
http://ghc.haskell.org/trac/ghc/ticket/6124
http://ghc.haskell.org/trac/ghc/ticket/6124#6124: Spurious non-exhaustive warning with GADT and newtypesFri, 25 May 2012 04:09:30 GMTjoeyadams<p>
This may be related to <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3927" title="bug: Incomplete/overlapped pattern warnings + GADTs = inadequate (new)">#3927</a> or similar, but here's another case where the compiler produces a "Pattern match(es) are non-exhaustive" warning for patterns on a GADT that are impossible to implement:
</p>
<pre class="wiki">newtype A = MkA Int
newtype B = MkB Char
data T a where
A :: T A
B :: T B
f :: T A -> A
f A = undefined
</pre><p>
This produces the following warning:
</p>
<pre class="wiki"> Warning: Pattern match(es) are non-exhaustive
In an equation for `f': Patterns not matched: B
</pre><p>
It is impossible to write a pattern for <tt>B</tt> because <tt>B :: T B</tt> does not match <tt>T A</tt>.
</p>
<p>
If I replace <tt>newtype</tt> with <tt>data</tt> for both <tt>A</tt> and <tt>B</tt>, the warning goes away. If I replace only one instance of either <tt>newtype</tt>, it will still produce the warning.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/6124#changelog
http://ghc.haskell.org/trac/ghc/ticket/6065
http://ghc.haskell.org/trac/ghc/ticket/6065#6065: Suggested type signature causes a type error (even though it appears correct)Mon, 30 Apr 2012 18:02:24 GMTtvynr<p>
The attached file, MWE.hs, contains an experiment attempting a rudimentary encoding of extensible ASTs in Haskell (without using compdata or a similar package relying upon <a class="missing wiki">OverlappingInstances?</a> and so forth). The definition of the upcast function appears to be correct. Compiling without a type signature produces a warning and the suggestion to include a type signature. Including the suggested type signature (which appears to be the correct one) causes a type error.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/6065#changelog
http://ghc.haskell.org/trac/ghc/ticket/6024
http://ghc.haskell.org/trac/ghc/ticket/6024#6024: Allow defining kinds alone, without a datatypeThu, 19 Apr 2012 16:12:01 GMTdreixel<p>
Sometimes we want to define a kind alone, and we are not interested in the datatype. In principle having an extra datatype around is not a big problem, but the constructor names will be taken, so they cannot be used somewhere else. A contrived example:
</p>
<pre class="wiki">data Code = Unit | Prod Code Code
data family Interprt (c :: Code) :: *
data instance Interprt Unit = Unit1
data instance Interprt (Prod a b) = Prod1 (Interprt a) (Interprt b)
</pre><p>
We're only interested in the constructors of the data family <tt>Interprt</tt>, but we cannot use the names <tt>Unit</tt> and <tt>Prod</tt> because they are constructors of <tt>Code</tt>.
</p>
<p>
The suggestion is to allow defining:
</p>
<pre class="wiki">data kind Code = Unit | Prod Code Code
</pre><p>
Such that <tt>Code</tt> is a kind, and not a type, and <tt>Unit</tt> and <tt>Prod</tt> are types, and not constructors.
</p>
<p>
Note that using "data kind" instead of just "kind" means the word "kind" does not have to be a reserved keyword.
</p>
<p>
You could also think you would want to have datatypes that should not be promoted:
</p>
<pre class="wiki">data K
data type T = K
</pre><p>
But I don't see a need for this, as the fact that the <tt>K</tt> constructor is promoted to a type does not prevent you from having a datatype named <tt>K</tt>.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/6024#changelog
http://ghc.haskell.org/trac/ghc/ticket/5957
http://ghc.haskell.org/trac/ghc/ticket/5957#5957: signatures are too permissiveThu, 22 Mar 2012 10:22:54 GMTmaeder<p>
ghc should reject the following (accidentally mistyped) signature, unless <tt>-XFlexibleContexts</tt> is used.
</p>
<pre class="wiki">flex :: Int -> Show a => a -> String
flex i a = show a ++ show i
</pre><p>
hugs and ghc version below 7 rejected this correctly:
</p>
<pre class="wiki"> All of the type variables in the constraint `Show a'
are already in scope (at least one must be universally quantified here)
(Use -XFlexibleContexts to lift this restriction)
In the type signature for `flex':
flex :: Int -> (Show a) => a -> String
</pre><p>
It is not Haskell98 nor Haskell2010 (I believe).
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/5957#changelog
http://ghc.haskell.org/trac/ghc/ticket/5927
http://ghc.haskell.org/trac/ghc/ticket/5927#5927: A type-level "implies" constraint on ConstraintsSun, 11 Mar 2012 16:55:32 GMTillissius<p>
I have a datatype:
</p>
<pre class="wiki">data Exists c where Exists :: c a => a -> Exists c
</pre><p>
I have an instance for it:
</p>
<pre class="wiki">instance Show (Exists Show) where
show (Exists a) = show a
</pre><p>
And that's alright, as far as it goes: any Exists Show can indeed itself be shown. But I want more. I want to be able to say:
</p>
<pre class="wiki">instance (c `Implies` Show) => Show (Exists c) where
show (Exists a) = show a
</pre><p>
In other words, I want to be able to say that any (Exists c) where the constraint c implies Show can be shown. For example, if Num still had a Show constraint, I wouldn't want to have to write a separate instance Show (Exists Num) to be able to show an Exists Num; I would want to be able to write a single instance (along the lines of the above) which works for both.
</p>
<p>
GHC clearly has this information: it lets me use a function of type <tt>forall a. Eq a => a -> r</tt> as one of type <tt>forall a. Ord a => a -> r</tt>, but not vice versa, so it knows that Ord implies Eq, but not vice versa. I've attached a file which demonstrates this and a couple of other examples.
</p>
<p>
What's not completely clear to me is what would be the appropriate way to be able to ask it about this. An Implies constraint to parallel the (~) constraint would work, but with what syntax? (Just straightforwardly call it Implies?) And what semantics -- what would be the kind of Implies? It's notable that in the above example its arguments aren't of type Constraint, but rather * -> Constraint, and for (* -> *) -> Constraint it could similarly work, and with MPTCs * -> * -> Constraint and (* -> *) -> (* -> *) -> Constraint and * -> (* -> *) -> Constraint and so on probably also make sense... but I have no idea how to formalize this, where the boundaries lie, and whether it makes any kind of sense. I can try to think harder about it if that would help, but hopefully the outlines of the situation are more immediately obvious to someone on the GHC team.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/5927#changelog
http://ghc.haskell.org/trac/ghc/ticket/5910
http://ghc.haskell.org/trac/ghc/ticket/5910#5910: Holes with other constraintsFri, 02 Mar 2012 10:59:29 GMTxnyhps<p>
Hello. As can be seen on <a class="ext-link" href="http://hackage.haskell.org/trac/ghc/wiki/Holes"><span class="icon"></span>http://hackage.haskell.org/trac/ghc/wiki/Holes</a> and <a class="ext-link" href="http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html"><span class="icon"></span>http://www.haskell.org/pipermail/glasgow-haskell-users/2012-January/021670.html</a>, we've been working on adding holes to GHC. I'm opening this ticket about a specific problem I've been having, and I hope someone has a suggestion of how to do it correctly.
</p>
<p>
As holes work quite similarly to implicit parameters (see the wiki-page for a comparison), we started out in the same way as implicit parameters. Typechecking of a hole generates a constraint (a new type of constraint), and the constraint solver will try to find the right type for each hole. The difference is that hole constraints never show up in a type, but their type is printed separately. This currently works correctly for simple typechecking, but it has some problems when other constraints are generated too. A simple example:
</p>
<pre class="wiki">test :: String
test = show _h
</pre><p>
Here, the <tt>_h</tt> denotes a hole named "h". If this function is defined like this inside a module it will currently fail:
</p>
<pre class="wiki">test2.hs:2:8:
No instance for (Show a0)
arising from a use of `show'
The type variable `a0' is ambiguous
Possible fix: add a type signature that fixes these type variable(s)
In the expression: show (_h)
In an equation for `test': test = show (_h)
Failed, modules loaded: none.
</pre><p>
The problem is that the <tt>Show</tt> constraint is still there. If the type signature is omitted and the monomorphism restriction off, we can see that the types found are:
</p>
<pre class="wiki">Found the following holes:
_h :: GHC.Show.Show a => a
...
test :: Show a => String
</pre><p>
The problem is the <tt>Show a</tt> that is irrelevant to the actual type of <tt>test</tt>, but nevertheless it's there.
</p>
<p>
How do other approaches handle this?
</p>
<p>
<strong>undefined</strong>:
</p>
<pre class="wiki">test :: String
test = show undefined
</pre><p>
Gives the same ambiguity error, even if the signature is omitted.
</p>
<p>
<strong>Implicit parameters</strong>:
</p>
<pre class="wiki">test = show ?h
</pre><p>
This works, but generates the following type signature:
</p>
<pre class="wiki">test :: (Show a, ?h::a) => String
</pre><p>
So, as I'd want to use it, this is wrong. It has the right ingredients, but I'd want:
</p>
<pre class="wiki">test :: (?h :: (Show a) => a) => String
</pre><p>
For implicit parameters the difference doesn't matter too much, as implicit parameters are still parameters: they still show up in the type signature. A hole is not required to be a parameter, so it's more important that every constraint only shows up where it's necessary.
</p>
<p>
So the problem is that I don't know how to select from the constraints only those that are applicable to the expression/function itself, and those that apply to which of the holes. I've tried typechecking all of the holes first, but I don't know how to determine how to change the constraint set after that. If you need more information about how it currently works, or have any feedback on this approach, please let me know. I'm still quite unfamiliar with the architecture of GHC. :)
</p>
<hr />
<p>
I'm attaching a patch against the master branch on git with my current work in case someone is interested in trying it. Note that the code generation is pretty much a stub and it will panic if you try to run a function with a hole. It will print the holes of an expression if you invoke <tt>:t</tt> (it doesn't currently print the holes when loading a module, but it should still print them with <tt>:t</tt> on a function from the module). Also, I do not recommend building stage 1 with this, as some packages have some issues. Easiest is to build stage 1 and the packages without these changes and then applying the patch and then building only stage 2.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/5910#changelog
http://ghc.haskell.org/trac/ghc/ticket/5610
http://ghc.haskell.org/trac/ghc/ticket/5610#5610: Improve "Unacceptable argument type in foreign declaration" error messageMon, 07 Nov 2011 15:48:30 GMTbgamari<p>
Using ghc <a class="changeset" href="http://ghc.haskell.org/trac/ghc/changeset/1ece7b27a11c6947f0ae3a11703e22b7065a6b6c/ghc" title="Fix validate by moving OPTIONS -fno-warn-tabs Validate fixed for Mac OS X ...">1ece7b27a11c6947f0ae3a11703e22b7065a6b6c</a>, zlib fails to build,
</p>
<pre class="wiki">$ cabal install zlib
Resolving dependencies...
Configuring zlib-0.5.3.1...
Preprocessing library zlib-0.5.3.1...
Building zlib-0.5.3.1...
[1 of 5] Compiling Codec.Compression.Zlib.Stream ( dist/build/Codec/Compression/Zlib/Stream.hs, dist/build/Codec/Compression/Zlib/Stream.o )
Codec/Compression/Zlib/Stream.hsc:857:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h inflateInit2_" c_inflateInit2_
:: StreamState -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:857:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h inflateInit2_" c_inflateInit2_
:: StreamState -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:857:1:
Unacceptable result type in foreign declaration: IO CInt
Safe Haskell is on, all FFI imports must be in the IO monad
When checking declaration:
foreign import ccall unsafe "static zlib.h inflateInit2_" c_inflateInit2_
:: StreamState -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:865:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h inflate" c_inflate
:: StreamState -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:865:1:
Unacceptable result type in foreign declaration: IO CInt
Safe Haskell is on, all FFI imports must be in the IO monad
When checking declaration:
foreign import ccall unsafe "static zlib.h inflate" c_inflate
:: StreamState -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:872:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h deflateInit2_" c_deflateInit2_
:: StreamState
-> CInt
-> CInt -> CInt -> CInt -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:872:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h deflateInit2_" c_deflateInit2_
:: StreamState
-> CInt
-> CInt -> CInt -> CInt -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:872:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h deflateInit2_" c_deflateInit2_
:: StreamState
-> CInt
-> CInt -> CInt -> CInt -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:872:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h deflateInit2_" c_deflateInit2_
:: StreamState
-> CInt
-> CInt -> CInt -> CInt -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:872:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h deflateInit2_" c_deflateInit2_
:: StreamState
-> CInt
-> CInt -> CInt -> CInt -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:872:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h deflateInit2_" c_deflateInit2_
:: StreamState
-> CInt
-> CInt -> CInt -> CInt -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:872:1:
Unacceptable result type in foreign declaration: IO CInt
Safe Haskell is on, all FFI imports must be in the IO monad
When checking declaration:
foreign import ccall unsafe "static zlib.h deflateInit2_" c_deflateInit2_
:: StreamState
-> CInt
-> CInt -> CInt -> CInt -> CInt -> Ptr CChar -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:884:1:
Unacceptable argument type in foreign declaration: CInt
When checking declaration:
foreign import ccall unsafe "static zlib.h deflate" c_deflate
:: StreamState -> CInt -> IO CInt
Codec/Compression/Zlib/Stream.hsc:884:1:
Unacceptable result type in foreign declaration: IO CInt
Safe Haskell is on, all FFI imports must be in the IO monad
When checking declaration:
foreign import ccall unsafe "static zlib.h deflate" c_deflate
:: StreamState -> CInt -> IO CInt
cabal: Error: some packages failed to install:
zlib-0.5.3.1 failed during the building phase. The exception was:
ExitFailure 1
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/5610#changelog
http://ghc.haskell.org/trac/ghc/ticket/5590
http://ghc.haskell.org/trac/ghc/ticket/5590#5590: "guarded instances": instance selection can add extra parameters to the classFri, 28 Oct 2011 05:19:55 GMTnfrisby<p>
Disclaimer: the same semantics can currently be achieved without this syntax. So this is mostly a Parser request, though I've made it a Type Checker request because some type errors would probably need to be aware of the language extension. More on this at the bottom.
</p>
<p>
We'll start with a demonstration. Just some ancillary declarations for now.
</p>
<pre class="wiki">class Sat t where dict :: t
data True; data False
type family Pred (p :: * -> *) a
type family Left a; type instance (Either l r) = l
type family Right a; type instance (Either l r) = r
data Path p a where
Here :: p a -> Path p a
L :: Path p l -> Path p (Either l r)
R :: Path p r -> Path p (Either l r)
</pre><p>
The objective of these declarations is to allow us to define some <tt>Pred</tt>icate <tt>p</tt> and use the <tt>Sat</tt> class to find a path leading through a tree of <tt>Either</tt>s to a type that satisfies that <tt>Pred</tt>icate.
</p>
<p>
These next three declarations use the new syntax, as I'm imagining it.
</p>
<pre class="wiki">-- NB new syntax: `guard' keyword, the pipe after the instance head,
-- and a comma-separated list of types after that
instance guard Sat (Path a)
| Pred p a, Pred (Path p) (Left a), Pred (Path p) (Right a)
-- now we match on the instance guards, using the same pipe syntax
instance Sat (p a) => Sat (Path p a) | True , satl , satr where
dict = Here dict
instance Sat (Path p l) => Sat (Path p (Either l r)) | False, True , satr where
dict = SL dict
instance Sat (Path p r) => Sat (Path p (Either l r)) | False, False, True where
dict = SR dict
</pre><p>
The <tt>guard</tt> declaration asserts that any instance of <tt>Sat</tt> with a head that <em>would</em> overlap a la <tt>OverlappingInstances</tt> with <tt>Path a</tt> shall be disambiguated via the comma-separated list of types following the pipe. In this example, the subsequent three instances, which would traditionally overlap, are indeed disambiguated by their additional "instance head guards" (cf. HList's type-level programming style: <a class="ext-link" href="http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap"><span class="icon"></span>AdvancedOverlap</a>).
</p>
<p>
We can currently simulate this syntax by declaring a variant class of `Sat' which takes an extra parameter and thread the instance guards through that. Unfortunately, this workaround is repetitive, misses out on the better type error messages possible with specific Type Checker support, and it's just a bother.
</p>
<pre class="wiki">class Sat_ a anno where dict_ :: anno -> a
instance (anno ~ (Pred p a, Pred (Path p) (Left a), Pred (Path p) (Right a)),
Sat_ (Found a) anno) => Sat (Path p a) where
dict = dict_ (undefined :: anno)
instance Sat (p a) => Sat_ (Path p a) (True, satl, satr) where
dict_ _ = Here dict
…
</pre><p>
In the spirit of <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/4259" title="feature request: Relax restrictions on type family instance overlap (new)">#4259</a>, <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/TypeFunctions/TotalFamilies">total type families</a>, and <a class="ext-link" href="http://www.haskell.org/haskellwiki/GHC/AdvancedOverlap"><span class="icon"></span>AdvancedOverlap</a>, this syntax could be enriched and thereby promoted to an actual Type Checker extension. Replacing the comma-separated list of types in the <tt>guard</tt> declaration with a sequence of contexts would be appropriate syntax for explicitly making instance selection sensitive to those contexts. The instance head guards could then just be a type boolean (wired-in to the compiler, now) indicating whether the context was satisfied. A <tt>True</tt> would bring that context's consequences to bear within both the instance's own context and its declarations. For example, we could do without the <tt>Left</tt> and <tt>Right</tt> type families.
</p>
<pre class="wiki">instance guard Sat (Path a)
| (Pred p a) (a ~ Either l r, Pred (Path p) l) (a ~ Either l r, Pred (Path p) r)
instance Sat (p a) => Sat (Path p a) | True satl satr where
dict = Here dict
…
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/5590#changelog
http://ghc.haskell.org/trac/ghc/ticket/5296
http://ghc.haskell.org/trac/ghc/ticket/5296#5296: Add explicit type applicationsSun, 03 Jul 2011 17:30:35 GMTdsf<p>
This example is derived from code in my application. It works, but I can't add a signature to it. In other places it is preventing some code from compiling at all.
</p>
<pre class="wiki">{-# LANGUAGE KindSignatures, MultiParamTypeClasses, RankNTypes #-}
{-# OPTIONS -Wall #-}
module Test where
class C t1 t2 m where method :: Int -> m t2
f :: forall t1 t2 (m :: * -> *). C t1 t2 m => Int -> m t2
f x = method x
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/5296#changelog
http://ghc.haskell.org/trac/ghc/ticket/5267
http://ghc.haskell.org/trac/ghc/ticket/5267#5267: Missing type checks for arrow command combinatorsWed, 22 Jun 2011 08:44:02 GMTpeteg<p>
Is this expected to work?
</p>
<pre class="wiki">{-# LANGUAGE Arrows #-}
module T where
import Prelude
import Control.Arrow
t = proc () ->
do rec x <- arr id <<< (| (arr id) (returnA -< x) |)
returnA -< x
t' = proc x ->
do x <- arr id <<< (| (arr id) (returnA -< x) |)
returnA -< x
t'' = proc x ->
do x <- arr id <<< (| (arr id) (returnA -< 3) |)
returnA -< x
t''' = proc x -> arr id <<< (| (arr id) (returnA -< 3) |)
</pre><p>
I get:
</p>
<pre class="wiki">/tmp/T.hs:8:18:
The type of the first argument of a command form has the wrong shape
Argument type: t_tX
In the command: (arr id) <<< ((|(arr id) ((returnA -< x))|))
In a stmt of a 'do' expression:
x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))
In a stmt of a 'do' expression:
rec {x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))}
/tmp/T.hs:12:14:
The type of the first argument of a command form has the wrong shape
Argument type: t_tG
In the command: (arr id) <<< ((|(arr id) ((returnA -< x))|))
In a stmt of a 'do' expression:
x <- (arr id) <<< ((|(arr id) ((returnA -< x))|))
In the expression:
proc x -> do { x <- (arr id) <<< ((|(arr id) ((returnA -< x))|));
returnA -< x }
/tmp/T.hs:16:14:
The type of the first argument of a command form has the wrong shape
Argument type: t_tq
In the command: (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In a stmt of a 'do' expression:
x <- (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In the expression:
proc x -> do { x <- (arr id) <<< ((|(arr id) ((returnA -< 3))|));
returnA -< x }
/tmp/T.hs:19:18:
The type of the first argument of a command form has the wrong shape
Argument type: t_k
In the command: (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In the expression:
proc x -> (arr id) <<< ((|(arr id) ((returnA -< 3))|))
In an equation for `t'''':
t''' = proc x -> (arr id) <<< ((|(arr id) ((returnA -< 3))|))
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/5267#changelog
http://ghc.haskell.org/trac/ghc/ticket/5248
http://ghc.haskell.org/trac/ghc/ticket/5248#5248: Infer type context in a type signatureThu, 09 Jun 2011 19:02:22 GMTgidyn<p>
If I have code such as
</p>
<pre class="wiki">class Foo f where
foo :: a -> f a
data Bar f a = Foo f => Bar {bar :: f a}
instance Foo (Bar f) where
foo a = Bar (foo a)
</pre><p>
GHC will demand <tt>Foo f =></tt> on the instance declaration, even though this can be inferred from the definition of Bar.
</p>
<p>
I understand <em>why</em> this is happening, but it should not be necessary to repeat information already given. Some code violates DRY dozens of times because of this limitation.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/5248#changelog
http://ghc.haskell.org/trac/ghc/ticket/4921
http://ghc.haskell.org/trac/ghc/ticket/4921#4921: report ambiguous type variables more consistentlyThu, 27 Jan 2011 07:21:18 GMTSaizan<pre class="wiki">{-# LANGUAGE MultiParamTypeClasses #-}
module Amb where
class C a b where
f :: (a,b)
instance C Int Char where
f = undefined
{-
x = fst f
/home/saizan/snippets/Amb.hs:7:8:
Ambiguous type variables `a', `b' in the constraint:
`C a b'
arising from a use of `f' at /home/saizan/snippets/Amb.hs:7:8
Possible cause: the monomorphism restriction applied to the following:
x :: a (bound at /home/saizan/snippets/Amb.hs:7:0)
Probable fix: give these definition(s) an explicit type signature
or use -XNoMonomorphismRestriction
Failed, modules loaded: none.
-}
{-
y = fst f :: Int
/home/saizan/snippets/Amb.hs:21:8:
No instance for (C Int b)
arising from a use of `f' at /home/saizan/snippets/Amb.hs:21:8
Possible fix: add an instance declaration for (C Int b)
In the first argument of `fst', namely `f'
In the expression: fst f :: Int
In the definition of `y': y = fst f :: Int
Failed, modules loaded: none.
-}
</pre><p>
Both x and y have the same problem, there isn't enough type information to let the typechecker decide on an instance, so it seems they should produce similar error messages.
</p>
<p>
In particular, the error for y is quite confusing since it can be reasonably interpreted as saying there's no type b for which there's an instance C Int b, which in fact is not true, so i think explicitly mentioning the ambiguity like in the first message would help many to understand the problem better.
</p>
<p>
I can see though that an "instance C Int b" could make sense, more often than C a b, so maybe "Possible fix: add an instance declaration for (C Int b)" should be conserved, even if it still has the problem of expressing that the second argument needs to be a variable.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/4921#changelog
http://ghc.haskell.org/trac/ghc/ticket/4894
http://ghc.haskell.org/trac/ghc/ticket/4894#4894: Missing improvement for fun. deps.Mon, 17 Jan 2011 03:16:09 GMTdiatchki<p>
The problem is illustrated by the following example:
</p>
<pre class="wiki">{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class F a b | a -> b
f :: (F a b, F a c) => a -> b -> c
f _ = id
Results in the following error:
Could not deduce (b ~ c)
from the context (F a b, F a c)
bound by the type signature for f :: (F a b, F a c) => a -> b -> c
at bug.hs:6:1-8
`b' is a rigid type variable bound by
the type signature for f :: (F a b, F a c) => a -> b -> c
at bug.hs:6:1
`c' is a rigid type variable bound by
the type signature for f :: (F a b, F a c) => a -> b -> c
at bug.hs:6:1
Expected type: b -> c
Actual type: b -> b
In the expression: id
In an equation for `f': f _ = id
</pre><p>
The issue seems to be related to Note [When improvement happens] in module <a class="missing wiki">TcInteract?</a>. It states that two "givens" do not interact for the purposes of improvement.
</p>
<p>
As far as I understand, the correct behavior should be to generate a new given equality, justified by the functional dependency on the class.
</p>
<p>
This is also related to bug <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1241" title="bug: Functional dependency Coverage Condition is lifted, and should not be (closed: fixed)">#1241</a>: in order to justify an improvement by functional dependency, we have to check that all instances are consistent with the dependency. Otherwise, the above function would turn into an "unsafe cast" function.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/4894#changelog
http://ghc.haskell.org/trac/ghc/ticket/4479
http://ghc.haskell.org/trac/ghc/ticket/4479#4479: Add Type Directed Name ResolutionSat, 06 Nov 2010 19:50:22 GMTgidyn<p>
A request to implement <a class="ext-link" href="http://hackage.haskell.org/trac/haskell-prime/wiki/TypeDirectedNameResolution"><span class="icon"></span>type-directed name resolution</a>, as <a class="ext-link" href="http://hackage.haskell.org/trac/haskell-prime/ticket/129"><span class="icon"></span>proposed</a> for Haskell'.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/4479#changelog
http://ghc.haskell.org/trac/ghc/ticket/4385
http://ghc.haskell.org/trac/ghc/ticket/4385#4385: Type-level natural numbersMon, 11 Oct 2010 23:22:51 GMTdiatchki<p>
Natural numbers at the type-level have many uses, especially in contexts where programmers need to manipulate data with statically known sizes. A simple form of this feature has been present in many programming languages for a long time (e.g., sub-range types in Pascal, array type in C, etc.). The feature is particularly useful when combined with polymorphism as illustrated by more recent programming languages (e.g., Cyclone, <a class="missing wiki">BlueSpec?</a>, Cryptol, Habit).
</p>
<p>
Existing features of Haskell's type system---such as polymorphism, kinds, and qualified types---make it particularly suitable for adding support for type level naturals in a natural way!
</p>
<p>
Indeed, there are quite a few Haskell libraries available on Hackage that implement support for type-level numbers in various forms. These libraries are being used by other packages and projects (e.g., the Kansas Lava project, and the type-safe bindings to the LLVM library).
</p>
<p>
Supporting natural number types directly in the compiler would help these projects, and others, by improving on the existing libraries in the following ways:
</p>
<ul><li>a standard implementation,
</li><li>a better notation,
</li><li>better error messages,
</li><li>a more efficient implementation,
</li><li>more complete support for numeric operations.
</li></ul><p>
I have started on an implementation of this feature, and my GHC branch is available in a darcs repository at the following URL:
</p>
<pre class="wiki">http://code.galois.com/darcs/ghc-type-naturals/
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/4385#changelog
http://ghc.haskell.org/trac/ghc/ticket/4347
http://ghc.haskell.org/trac/ghc/ticket/4347#4347: Bug in unification of polymorphic and not-yet-polymorphic typeMon, 27 Sep 2010 21:36:08 GMTdolio<p>
The new type checker in GHC 7 seems to reject some cases of impredicative instantiation that prior versions allowed. I was initially alerted to this by Simon Marlow, who sent a patch for vector-algorithms removing a use of <tt>($)</tt> where it would have to be instantiated impredicatively.
</p>
<p>
Initially, I thought this was due to a planned removal of impredicativity, but this cannot be the case, because:
</p>
<pre class="wiki">const :: a -> (forall b. b) -> a
</pre><p>
is accepted by the type checker. However, the simple:
</p>
<pre class="wiki">id :: (forall a. a) -> (forall b. b)
</pre><p>
is not, giving an error message:
</p>
<pre class="wiki"> Couldn't match type `b' with `forall a. a'
`b' is a rigid type variable bound by
an expression type signature at <interactive>:1:32
In the expression: id :: (forall a. a) -> (forall b. b)
</pre><p>
This would seem to indicate that the type is being rewritten to:
</p>
<pre class="wiki">forall b. (forall a. a) -> b
</pre><p>
and then the <tt>forall a. a</tt> matched with the bare <tt>b</tt>. It is, of course, fine to rewrite the type this way, since the two are isomorphic, but it is unfortunate that it causes the checker to reject what would otherwise be a valid instantiation.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/4347#changelog
http://ghc.haskell.org/trac/ghc/ticket/4259
http://ghc.haskell.org/trac/ghc/ticket/4259#4259: Relax restrictions on type family instance overlapMon, 16 Aug 2010 14:43:56 GMTlilac<p>
The following reduced fragment of some real code is rejected, but could be accepted, by GHC:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
data True
type family LessEq a b :: *
type instance LessEq a a = True
type instance LessEq (f a) (f b) = LessEq a b
</pre><p>
GHC says:
</p>
<pre class="wiki"> Conflicting family instance declarations:
type instance LessEq a a
-- Defined at /home/richards/.random/tf.hs:5:14-19
type instance LessEq (f a) (f b)
-- Defined at /home/richards/.random/tf.hs:6:14-19
</pre><p>
This is entirely in line with the documentation, which requires the RHS to be structurally equivalent in the case of overlap. However, this rule is too restrictive. In the absence of -XUndecidableInstances, neither termination nor soundness would be sacrificed if the rule were relaxed to require extensional equality /after/ expanding the types as far as possible.
</p>
<p>
In particular (absent -XUndecidableInstances), such an expansion must terminate for the same reason that type families terminate in general. For soundness, suppose the resulting system is unsound, and consider the smallest type family application which has two possible distinct expanded types. We know the RHS of those types are equal after a partial expansion of only smaller (hence sound by minimality) type family applications, resulting in a contradiction.
</p>
<p>
In order to retain soundness in the presence of -XUndecidableInstances, any pair of type instances, where either instance could not be compiled without -XUndecidableInstances, would continue to use the current syntactic equality rule.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/4259#changelog
http://ghc.haskell.org/trac/ghc/ticket/4020
http://ghc.haskell.org/trac/ghc/ticket/4020#4020: Please consider adding support for local type synonymsTue, 27 Apr 2010 00:33:29 GMTnr<p>
I would really like to be able to put a type synonym in a where clause. I'm willing to specify <tt>LANGUAGE ScopedTypeVariables, LiberalTypeSynonyms</tt>.
</p>
<p>
For an example use case, please see line 202 of the attachment.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/4020#changelog
http://ghc.haskell.org/trac/ghc/ticket/3545
http://ghc.haskell.org/trac/ghc/ticket/3545#3545: As-patterns for type signaturesSun, 27 Sep 2009 21:14:30 GMTLouisWasserman<p>
The proposal: in any type signature, the presence of type variable
</p>
<p>
x@pat
</p>
<p>
matches the type specified by pat, and replaces any occurrences of the type variable x with pat. In particular, this might be comparable to defining
</p>
<p>
type x (free variables in pat) = pat
</p>
<p>
with scope solely to the right of the as-pattern. Alternately, it might be compared to an equality constraint (x ~ pat).
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/3545#changelog
http://ghc.haskell.org/trac/ghc/ticket/1928
http://ghc.haskell.org/trac/ghc/ticket/1928#1928: Confusing type error messageSun, 25 Nov 2007 14:44:33 GMTjosef<p>
The following code (which is part of a bigger module) needs scoped type variables to compile.
</p>
<pre class="wiki">run_state :: forall a s. State s a -> s -> (a,s)
run_state m s = observe_monad unit_op bind_op m where
unit_op v = (v,s)
bind_op :: BindOp (StateE s) a (a,s)
bind_op Get k = run_state (k s) s
bind_op (Put s1) k = run_state (k ()) s1
</pre><p>
However, forgetting to turn on scoped type variables will give a very confusing error message:
</p>
<pre class="wiki">Unimo.hs:56:36:
Couldn't match expected type `s1' against inferred type `s'
`s1' is a rigid type variable bound by
the type signature for `bind_op' at Unimo.hs:55:28
`s' is a rigid type variable bound by
the type signature for `run_state' at Unimo.hs:52:22
In the first argument of `k', namely `s'
In the first argument of `run_state', namely `(k s)'
In the expression: run_state (k s) s
</pre><p>
Line 52 is the type signature of run_state and line 55 is the type signature of bind_op. The error message talks about a type variable `s1' which isn't mentioned anywhere. I guess the reason for this is that we have name collision and this is ghc's way of trying to tell the two variables apart. I don't think it works that well though. But I'm afraid I don't have any suggestion on how to make it better.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1928#changelog
http://ghc.haskell.org/trac/ghc/ticket/1894
http://ghc.haskell.org/trac/ghc/ticket/1894#1894: Add a total order on type constructorsWed, 14 Nov 2007 19:22:11 GMTguest<p>
Several proposals for <a class="wiki" href="http://ghc.haskell.org/trac/ghc/wiki/ExtensibleRecords">ExtensibleRecords</a> can be implemented as libraries if type constructors can be ordered globally.
</p>
<p>
This proposal is to add built-in types:
</p>
<pre class="wiki">data LabelLT
data LabelEQ
data LabelGT
type family LabelCMP
</pre><p>
such that, for any two datatypes
</p>
<pre class="wiki">data N = N
data M = M
</pre><p>
the instance <tt>LabelCMP N M</tt> takes one of the values <tt>LabelLT, LabelEQ, LabelGT</tt> depending on the lexicographic ordering on the fully-qualified names of <tt>N</tt> and <tt>M</tt>.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1894#changelog
http://ghc.haskell.org/trac/ghc/ticket/1614
http://ghc.haskell.org/trac/ghc/ticket/1614#1614: Type checker does not use functional dependency to avoid ambiguityTue, 14 Aug 2007 21:59:39 GMTguest<p>
Compiling the following module gives an error
</p>
<pre class="wiki">module X where
class C a | -> a
instance C Int
unC :: (C a) => a -> Int
unC i = undefined
test :: Int
test = unC undefined
</pre><p>
Error message:
</p>
<pre class="wiki">X.hs:13:7:
Ambiguous type variable `a' in the constraint:
`C a' arising from a use of `unC' at X.hs:13:7-19
Probable fix: add a type signature that fixes these type variable(s)
</pre><p>
But that is just plain wrong. The functional dependency in the definition of C forces a to be Int. No other type is possible. So what's ambiguous about that?
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1614#changelog
http://ghc.haskell.org/trac/ghc/ticket/1451
http://ghc.haskell.org/trac/ghc/ticket/1451#1451: Provide way to show the origin of a constraintFri, 22 Jun 2007 11:25:14 GMTiampure@…<p>
For a complex type (A b, C d, E e) => Something a b e -> Int, provide a way to given the query:
where does A b come from? Respond with the line number of a function that causes that constraint. This should of course also work for non-Haskell 98 constraints.
</p>
<p>
This issue comes up when one by accident calls a function in the wrong layer of a monadic transformer stack.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1451#changelog
http://ghc.haskell.org/trac/ghc/ticket/1404
http://ghc.haskell.org/trac/ghc/ticket/1404#1404: allow more type signaturesFri, 01 Jun 2007 19:55:37 GMTIsaac Dupree<p>
(idea triggered by <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/393" title="feature request: functions without implementations (new)">#393</a>)
</p>
<p>
Allow multiple copies of a type-signature in a module, such that it is an error if they're not equivalent, but they don't have to be syntactically equal (
<tt>f :: ShowS</tt>
<tt>f :: String -> String</tt>
is okay).
</p>
<p>
It would also be nice to allow any name in scope at top-level (even if imported) to be given a type signature. But that raises a question: can these type signatures give a more specific type than that of the raw imported function, the way normal function type signatures can with regards to their implementation?
</p>
<p>
Use cases: (1. making sure multiple implementations give the same interface, generally varying by #ifdef) (2. asserting that something's type can be specified in two different weird ways). I don't really want to abandon having a type-signature right above every function definition even if it is a duplicate.
</p>
<p>
(1.) would be fixed by allowing type signatures in export lists instead. I suppose these could be more restrictive than in the module and not affect the module, e.g.
</p>
<pre class="wiki">module X (idN :: Int -> Int, true) where
idN n = n
true :: Bool
true = idN True
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/1404#changelog
http://ghc.haskell.org/trac/ghc/ticket/1330
http://ghc.haskell.org/trac/ghc/ticket/1330#1330: Impredicativity bug: Church2 test gives a rather confusing error with the HEADSat, 05 May 2007 15:23:10 GMTigloo<p>
The Church2 test gives a rather confusing error with the HEAD:
</p>
<pre class="wiki">Church2.hs:27:14:
Couldn't match expected type `CNat'
against inferred type `(a -> a) -> a -> a'
Expected type: CNat -> CNat
Inferred type: CNat -> CNat
In the first argument of `n', namely `(mul m)'
In the expression: n (mul m) n1
</pre><p>
In particular the lines
</p>
<pre class="wiki"> Expected type: CNat -> CNat
Inferred type: CNat -> CNat
</pre><p>
are confusing, and I'm not sure why it's giving two expected/inferred pairs of types.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1330#changelog
http://ghc.haskell.org/trac/ghc/ticket/816
http://ghc.haskell.org/trac/ghc/ticket/816#816: Weird fundep behavior (with -fallow-undecidable-instances)Thu, 06 Jul 2006 19:04:37 GMTnibro<p>
I encounter a strange behavior with functional dependencies. Consider this program
</p>
<pre class="wiki">class Foo x y | x -> y where
foo :: x -> y
class Bar x y where
bar :: x -> y -> Int
instance (Foo x y, Bar y z) => Bar x z where
bar x z = bar (foo x) z
</pre><p>
Compiling (with 6.4.2, -fallow-undecidable-instances and -fglasgow-exts) I get the following error message:
</p>
<pre class="wiki">Foo.hs:12:0:
Context reduction stack overflow; size = 21
Use -fcontext-stack20 to increase stack size to (e.g.) 20
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:11-13
[... same thing 20 times ...]
`$dBar :: Bar y z' arising from use of `bar' at Foo.hs:13:11-13
`bar :: {bar at [y z]}' arising from use of `bar' at Foo.hs:13:11-13
When trying to generalise the type inferred for `bar'
Signature type: forall x y z. (Foo x y, Bar y z) => x -> z -> Int
Type to generalise: x -> z -> Int
In the instance declaration for `Bar x z'
</pre><p>
The declaration requires undecidable instances, but I doubt that the problem comes from that. What makes it even more weird is that I can get this to compile, and behave as expected, if I do one of a) declare an instance of Bar for any type, or
b) add an explicit type signature (foo x :: y) in the definition of Bar. The first seems weird since how could a different, unrelated instance affect the typeability of the second instance? The second, b), is weird since by the FD x -> y we should already know that foo x :: y.
</p>
<p>
Same behavior in GHC 6.4.1. Hugs (with -98 +O) accepts the code.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/816#changelog
http://ghc.haskell.org/trac/ghc/ticket/589
http://ghc.haskell.org/trac/ghc/ticket/589#589: Various poor type error messagesWed, 07 Dec 2005 11:40:23 GMTPeter A Jonsson [pj@…<p>
Hello,
</p>
<p>
I read the summary of the survey and noticed you wanted feedback on
where error messages could be improved. I looked up some (simple)
examples of type errors and ran them through ghc. I do not make any
claims to be an HCI expert, just a mere mortal with an opinion.
</p>
<p>
<strong>Type error 1</strong>
</p>
<p>
Code:
</p>
<pre class="wiki">1 module Test2 where
2
3 fib n = if (3 > n) then 1 else (fib (n - 1) + fib (n - 2))
4 k = fib 's'
</pre><p>
Error message:
</p>
<pre class="wiki">Test2.hs:4:
No instance for (Num Char)
arising from use of `fib' at Test2.hs:4
In the definition of `k': k = fib 's'
</pre><p>
This isn't a bad error message in my humble opinion, it does pinpoint
that I'm doing something wrong in line 4, and that there isn't an
instance for Num Char doesn't come as a surprise. However I think it
could have been more helpful by telling me that I tried to pass a Char
to a function which expected an (Ord a, Num a) => a as its parameter.
</p>
<p>
<strong>Type error 2</strong>
</p>
<p>
Code:
</p>
<pre class="wiki">1 module Test4 where
2
3 k :: Int -> Int
4 k l = 2.0*l
</pre><p>
Error message:
</p>
<pre class="wiki">Test4.hs:4:
No instance for (Fractional Int)
arising from the literal `2.0' at Test4.hs:4
In the first argument of `(*)', namely `2.0'
In the definition of `k': k l = 2.0 * l
</pre><p>
One reason this kind of error could happen is an inexperienced user
declaring the wrong type for his function, or not knowing that 2.0
would be interpreted as a Fractional.
</p>
<p>
<strong>Type error 3</strong>
</p>
<p>
Code:
</p>
<pre class="wiki">1 module Test7 where
2
3 len' xs = head (xs) + (length xs)
4 o = len' "GH"
</pre><p>
Error message:
</p>
<pre class="wiki">Test7.hs:4:
Couldn't match `Int' against `Char'
Expected type: [Int]
Inferred type: [Char]
In the first argument of `len'', namely `"GH"'
In the definition of `o': o = len' "GH"
</pre><p>
I ran this through Hugs version November 2002 and got this error
message:
</p>
<pre class="wiki">ERROR "Test7.hs":4 - Type error in application
*** Expression : len' "GH"
*** Term : "GH"
*** Type : String
*** Does not match : [Int]
</pre><p>
I find the Hugs message more clear, but that might be my background.
</p>
<p>
<strong>Type error 4</strong>
</p>
<p>
Code:
</p>
<pre class="wiki">1 module Test8 where
2
3 f = head 3
</pre><p>
Error message:
</p>
<pre class="wiki">Test8.hs:3:
No instance for (Num [a])
arising from the literal `3' at Test8.hs:3
Possible cause: the monomorphism restriction applied to the following:
f :: a (bound at Test8.hs:3)
Probable fix: give these definition(s) an explicit type signature
In the first argument of `head', namely `3'
In the definition of `f': f = head 3
</pre><p>
This one I find outright scary. For "wrong = div 3 8 + 1/2" it gives
an error message that somewhat helps me guess the error, but the above
doesn't even come close to helping me.
</p>
<p>
/ Peter
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/589#changelog
http://ghc.haskell.org/trac/ghc/ticket/472
http://ghc.haskell.org/trac/ghc/ticket/472#472: Supertyping of classesThu, 20 Oct 2005 18:34:34 GMTnobody<p>
see
<a class="ext-link" href="http://repetae.net/john/recent/out/supertyping.html"><span class="icon"></span>Supertyping Suggestion for Haskell</a>
</p>
<p>
example:
</p>
<pre class="wiki">class Num a <= Group a where
(+) :: a -> a -> a
negate :: a -> a
</pre><p>
apart from multiple inheritance, it could work like this:
</p>
<pre class="wiki">import Prelude hiding ((+),negate)
import qualified Prelude ((+),negate)
class Group a where
(+) :: a -> a -> a
negate :: a -> a
instance Num a => Group a where
(+) = (Prelude.+)
negate = Prelude.negate
</pre><ul><li>coeus_at_gmx_de
</li></ul>Resultshttp://ghc.haskell.org/trac/ghc/ticket/472#changelog
http://ghc.haskell.org/trac/ghc/ticket/393
http://ghc.haskell.org/trac/ghc/ticket/393#393: functions without implementationsThu, 26 May 2005 10:53:23 GMTc_maeder<pre class="wiki">Allow to declare a function by only supplying its type
signature.
This feature shall enhance rapid prototyping by fixing
an interface but leaving some functions unimplemented.
Currently this can be (only) simulated by supplying
dummy implementations, like
f :: ...
f = undefined
Since it is possible to supply dummy data types by
"data T" (not followed by "="), allowing functions
without implementations seems almost to be a logical
consequence. Surely, the compiler should emit warnings
for missing implementations.
It would be nice if such function declarations via type
signatures could be repeated at any position within a
module.
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/393#changelog
http://ghc.haskell.org/trac/ghc/ticket/345
http://ghc.haskell.org/trac/ghc/ticket/345#345: GADT - fundep interactionFri, 08 Apr 2005 10:02:38 GMTbring<pre class="wiki">GADTs and fundeps don't seem to interact in the way
that I (perhaps naively) expect. I expected that for
each case, the type variables would be instantiated
according to the type of the constructors, and then the
fundep would be used to figure out the result type.
{-# OPTIONS_GHC -fglasgow-exts #-}
data Succ n
data Zero
class Plus x y z | x y -> z
instance Plus Zero x x
instance Plus x y z => Plus (Succ x) y (Succ z)
infixr 5 :::
data List :: * -> * -> * where
Nil :: List a Zero
(:::) :: a -> List a n -> List a (Succ n)
append :: Plus x y z => List a x -> List a y -> List a z
append Nil ys = ys
append (x ::: xs) ys = x ::: append xs ys
{-
GHC 6.4 says:
Couldn't match the rigid variable `y' against `Succ z'
`y' is bound by the type signature for `append'
Expected type: List a y
Inferred type: List a (Succ z)
In the expression: x ::: (append xs ys)
In the definition of `append': append (x ::: xs) ys
= x ::: (append xs ys)
-}
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/345#changelog
http://ghc.haskell.org/trac/ghc/ticket/344
http://ghc.haskell.org/trac/ghc/ticket/344#344: arrow notation: incorrect scope of existential dictionariesThu, 07 Apr 2005 20:39:35 GMTnobody<pre class="wiki">ghc-6.4: panic! (the `impossible' happened, GHC version
6.4):
cgPanic
deref{v a1yz}
static binds for:
local binds for:
SRT labelghc-6.4: panic! (the `impossible'
happened, GHC version 6.4):
initC: srt
Please report it as a compiler bug to
glasgow-haskell-bugs@haskell.org,
or http://sourceforge.net/projects/ghc/.
I've attached a test driver that can reproduce the problem.
-- Esa Pulkkinen <esa.pulkkinen@kotiposti.net>
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/344#changelog