GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=infoneeded&status=merge&status=new&status=patch&component=Compiler+(Type+checker)&milestone=7.6.2&group=status&order=priority
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?status=infoneeded&status=merge&status=new&status=patch&component=Compiler+(Type+checker)&milestone=7.6.2&group=status&order=priority
Trac 1.0.1
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/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/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/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/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/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/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/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/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/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/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
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/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