GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?component=Compiler+(Type+checker)&milestone=6.10+branch&group=status&order=resolution
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?component=Compiler+(Type+checker)&milestone=6.10+branch&group=status&order=resolution
Trac 1.0.1
http://ghc.haskell.org/trac/ghc/ticket/1470
http://ghc.haskell.org/trac/ghc/ticket/1470#1470: Overlapping (etc) instancesFri, 29 Jun 2007 18:58:57 GMTigloo<p>
This self-contained module:
</p>
<pre class="wiki">{-# LANGUAGE FlexibleInstances, OverlappingInstances, UndecidableInstances #-}
module Foo where
class Sat a
class Data ctx a
instance Sat (ctx Char) => Data ctx Char
instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]
class Data FooD a => Foo a
data FooD a = FooD
instance Foo t => Sat (FooD t)
instance Data FooD a => Foo a
instance Foo a => Foo [a]
instance Foo [Char]
</pre><p>
gives this error in the HEAD (and a similar, but less helpful, error in 6.6):
</p>
<pre class="wiki">$ ghc -c Foo.hs
Foo.hs:18:0:
Overlapping instances for Foo [a]
arising from the superclasses of an instance declaration
at Foo.hs:18:0
Matching instances:
instance [overlap ok] (Foo a) => Foo [a]
-- Defined at Foo.hs:18:0-30
instance [overlap ok] Foo [Char] -- Defined at Foo.hs:19:0-33
(The choice depends on the instantiation of `a'
Use -fallow-incoherent-instances to use the first choice above)
In the instance declaration for `Foo [a]'
</pre><p>
Simon writes:
</p>
<pre class="wiki">The reason is this:
In the instance for Foo [a]
we need a superclass (Data FooD [a])
using the instance for Data, we therefore need
(Sat (FooD [a], Data FooD a)
But we are given Foo a, and hence its superclass Data FooD a
So that leaves (Sat (FooD [a]))
Using the instance for Sat means
we need (Foo [a])
At that point GHC says there are two instances that match Foo [a], and which one
to choose depends on how you instantiate a.
What we wanted was to "tie the knot" and use Foo [a] recursively, the very one
we are constructing. GHC does that when solving Foo [a], but not when
constructing it.
This is a good point, I will think about it. It's a bit delicate. Meanwhile,
can you Trac it? It's a nice example.
</pre><p>
A larger module showing how the instances above can be desirable in a real program is this (requires the syb-with-class package from hackage):
</p>
<pre class="wiki">{-# LANGUAGE TemplateHaskell, FlexibleInstances, CPP,
OverlappingInstances, UndecidableInstances #-}
module Main where
import Data.Generics.SYB.WithClass.Basics
import Data.Generics.SYB.WithClass.Instances ()
data Element = Elem String [Element]
| CData String
deriving Show
class Data XmlD a => Xml a where
toXml :: a -> [Element]
toXml = defaultToXml
data XmlD a = XmlD { toXmlD :: a -> [Element] }
xmlProxy :: Proxy XmlD
xmlProxy = error "xmlProxy"
instance Xml t => Sat (XmlD t) where
dict = XmlD { toXmlD = toXml }
defaultToXml :: Xml t => t -> [Element]
defaultToXml x = [Elem (constring $ toConstr xmlProxy x)
(concat $ gmapQ xmlProxy (toXmlD dict) x)]
-----
instance Data XmlD t => Xml t
#ifdef STRING
instance Xml String where
toXml x = [Elem "string" [CData x]]
#endif
#ifdef LIST
instance Xml a => Xml [a] where
toXml = concatMap toXml
#endif
main :: IO ()
main = do print $ toXml (Just True)
print $ toXml [True, False]
print $ toXml "foo"
</pre><p>
which allows us to specialise XML marshalling for either lists (ignoring all the (:) and [] constructors) or strings (turn them into CData), but not both:
</p>
<pre class="wiki">$ ghci -v0 -DLIST z.hs
*Main> main
[Elem "Just" [Elem "True" []]]
[Elem "True" [],Elem "False" []]
[Elem "f" [],Elem "o" [],Elem "o" []]
*Main>
$ ghci -v0 -DSTRING z.hs
*Main> main
[Elem "Just" [Elem "True" []]]
[Elem "(:)" [Elem "True" [],Elem "(:)" [Elem "False" [],Elem "[]" []]]]
[Elem "string" [CData "foo"]]
*Main>
$ ghci -v0 -DLIST -DSTRING z.hs
[overlapping instances error]
</pre><p>
If we replace the
</p>
<pre class="wiki">instance Xml a => Xml [a] where
</pre><p>
line with
</p>
<pre class="wiki">instance (Xml a, Xml [a]) => Xml [a] where
</pre><p>
then everything seems to work out, but this feels a little dodgy.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1470#changelog
http://ghc.haskell.org/trac/ghc/ticket/1537
http://ghc.haskell.org/trac/ghc/ticket/1537#1537: do notation translationMon, 16 Jul 2007 00:56:44 GMTIsaac Dupree<p>
&
Really there are two things:
</p>
<p>
Normally, (do True) fails to compile in GHC because there is no Monad Bool, whereas Haskell-98 translates it to (True).
</p>
<p>
With <tt>-fno-implicit-prelude</tt>, ( according to <a class="ext-link" href="http://comonad.com/reader/2007/parameterized-monads-in-haskell/"><span class="icon"></span>http://comonad.com/reader/2007/parameterized-monads-in-haskell/</a> ):
</p>
<p>
"""
Caveat: It appears that GHC enforces the fact that the arguments and results of (>>=) must have a signature like
</p>
<p>
(>>=) :: forall m a. (...) => m a -> (a -> m b) -> m b
</p>
<p>
insofar as when you use the do-sugar, your types will not be able to vary. Ideally it should be able to get by with a more liberal signature, but it seems like no one has needed it before now.
"""
</p>
<p>
I think do-notation will be the simplest sugar (from one point of view at least) when it just translates to (>;=), (>>), fail, and let..in.. as specified in Haskell98 (or non-Prelude-qualified when <tt>-fno-implicit-prelude</tt>, of course).
</p>
<p>
It appears <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/303" title="bug: Rebindable syntax doesn't work as advertised (closed: duplicate)">#303</a> was an older similar problem. Also, maybe the behavior (in the new version) should be explicitly documented somewhere in the User's Guide.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1537#changelog
http://ghc.haskell.org/trac/ghc/ticket/1608
http://ghc.haskell.org/trac/ghc/ticket/1608#1608: Newtype deriving error messages coming out too lateFri, 10 Aug 2007 08:17:04 GMTsimonpj<p>
Consider this
</p>
<pre class="wiki">newtype Ego a = Ego a deriving (Ord)
f :: Ord a => Ego a -> Ego a -> Bool
f e1 e2 = e1 < e2
</pre><p>
GHC 6.7 reports an error like this:
</p>
<pre class="wiki"> Could not deduce (Eq (Ego a)) from the context (Ord a)
arising from a use of `<' at Foo10.hs:6:10-16
In the expression: e1 < e2
In the definition of `f': f e1 e2 = e1 < e2
</pre><p>
This error should have come when you gave the instance decl. The reason is that GHC's newtype deriving is generating an instance like
</p>
<pre class="wiki">instance Eq (Ego a) => Ord (Ego a)
</pre><p>
It would make more sense to report the missing instance for Eq right there, rather than abstracting over it.
</p>
<p>
Thanks to Dougal Stanton for pointing this out: <a class="ext-link" href="http://www.haskell.org/pipermail/haskell-cafe/2007-August/030224.html"><span class="icon"></span>http://www.haskell.org/pipermail/haskell-cafe/2007-August/030224.html</a>
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1608#changelog
http://ghc.haskell.org/trac/ghc/ticket/1624
http://ghc.haskell.org/trac/ghc/ticket/1624#1624: internal error caused by adding an instance to a type class with a functional dependency and a default methodTue, 21 Aug 2007 16:12:26 GMTint-e<p>
I've got trouble with the following program:
</p>
<pre class="wiki">{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
class Foo a b | a -> b where
foo :: a -> b
foo = undefined
instance Foo a (Maybe a)
</pre><p>
This results in a type checking error, and an internal error:
</p>
<pre class="wiki">xx.hs:2:0:
Couldn't match expected type `b' (a rigid variable)
against inferred type `Maybe a'
`b' is bound by the class declaration for `Foo'
When using functional dependencies to combine
Foo a (Maybe a), arising from the instance declaration at x.hs:8:0
Foo a b,
arising from is bound by the class declaration for `Foo'
at x.hs:(2,0)-(4,18)
[snip]
x.hs:6:0:
GHC internal error: `Main.$dmfoo' is not in scope
In the expression: Main.$dmfoo
In the definition of `foo': foo = Main.$dmfoo
In the definition for method `foo'
</pre><p>
Slightly less convincing variations on the scheme are
</p>
<pre class="wiki">class Foo a b | a -> b
instance Foo a (Maybe a)
foo :: Foo a b => a -> b
foo = undefined
class Bar a b c
instance (Foo a b, Foo b c) => Bar a b c
</pre><p>
Both the definition of <tt>foo</tt> and the instance declaration of <tt>Bar</tt> give a type checking error "when combining functional dependencies".
</p>
<p>
Apparently <tt>ghc</tt> doesn't use functional dependencies to simplify the contexts of user supplied type signatures; I think the above examples indicate that it should.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1624#changelog
http://ghc.haskell.org/trac/ghc/ticket/1722
http://ghc.haskell.org/trac/ghc/ticket/1722#1722: Code using type synonym families requires workarounds to compileThu, 20 Sep 2007 12:41:40 GMTtomasz.zielonka@…<p>
I am trying to use type synonym families to create GADTs that can be used interchangably as both typed and untyped ASTs for a small programming language. Here are the (cut down & simplified) definitions:
</p>
<pre class="wiki">data Typed
data Untyped
type family TU a b :: *
type instance TU Typed b = b
type instance TU Untyped b = ()
-- A type witness type, use eg. for pattern-matching on types
data Type a where
TypeInt :: Type Int
TypeBool :: Type Bool
TypeString :: Type String
TypeList :: Type t -> Type [t]
data Expr :: * -> * -> * {- tu a -} where
Const :: Type a -> a -> Expr tu (TU tu a)
Var2 :: String -> TU tu (Type a) -> Expr tu (TU tu a)
</pre><p>
It mostly works, which still amazes me, but there are some small glitches. For example in some cases I have to use <strong>(TU Typed Bool)</strong> instead of
<strong>Bool</strong>, even if they should be equal (<strong>type instance TU Typed b = b</strong>). In other cases I have to artificially restrict or generalize functions' type signatures. Or I have to put type signatures in patterns. The biggest problem is that it isn't obvious which workaround is needed in a given case. For some cases I don't have a satisfactory workaround yet.
</p>
<p>
Perhaps these problems simply reflect immaturity of type synonym family support in GHC, but, on the other hand, it may be some simple bug which could be fixed for GHC 6.8.
</p>
<p>
I've created a set of test files which I will attach to this ticket. Run check.sh to see how GHC handles the original (inteded) code and the workarounds. But first set the path to ghc in the script.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1722#changelog
http://ghc.haskell.org/trac/ghc/ticket/1723
http://ghc.haskell.org/trac/ghc/ticket/1723#1723: type unsafety with type family + GADTThu, 20 Sep 2007 21:50:26 GMTzunino@…<p>
Here's <em>unsafeCoerce</em>:
</p>
<pre class="wiki">type family Const a
type instance Const a = ()
data T a where T :: a -> T (Const a)
coerce :: forall a b . a -> b
coerce x = case T x :: T (Const b) of
T y -> y
</pre><p>
Tested with GHC 6.9.20070918
</p>
<p>
Maybe, see also <a class="new ticket" href="http://ghc.haskell.org/trac/ghc/ticket/345" title="bug: GADT - fundep interaction (new)">#345</a>
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1723#changelog
http://ghc.haskell.org/trac/ghc/ticket/1772
http://ghc.haskell.org/trac/ghc/ticket/1772#1772: GHC doesn't like 'inline' type function applicationsThu, 11 Oct 2007 21:45:15 GMTjpbernardy<pre class="wiki">{-# LANGUAGE TypeFamilies #-}
import Prelude hiding (foldl, foldr, foldl1, foldr1, mapM_, sequence_,
elem, notElem, concat, concatMap, and, or, any, all,
sum, product, maximum, minimum)
import Data.Monoid
type family Element t
class Foldable t where
foldMap :: Monoid m => (Element t -> m) -> t -> m
foldr :: (Element t -> b -> b) -> b -> t -> b
-- foldr :: Element t ~ a => (a -> b -> b) -> b -> t -> b
foldr f z t = appEndo (foldMap (Endo . f) t) z
</pre><p>
GHC chokes on the above module. If the signature of foldr is replaced by the commented one, GHC is happy. It seems to me that the two expressions should be equivalent.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1772#changelog
http://ghc.haskell.org/trac/ghc/ticket/1815
http://ghc.haskell.org/trac/ghc/ticket/1815#1815: Occurs check error from equality constraintWed, 31 Oct 2007 08:14:22 GMTguest<p>
I was writing that manipulates witnesses for equality constraints,
and saw some occurs check errors for equations matching my constraints.
(This is with ghc-6.9.20071025).
</p>
<pre class="wiki">Bug.hs:19:31:
Occurs check: cannot construct the infinite type: n = Sum Z n
In the pattern: Refl
In a case alternative: Refl -> Refl
In the expression: case zerol n of Refl -> Refl
</pre><p>
Here is the program producing that error:
</p>
<pre class="wiki">{-# OPTIONS -fglasgow-exts #-}
module Bug where
data Z
data S a
type family Sum n m
type instance Sum n Z = n
type instance Sum n (S m) = S (Sum n m)
data Nat n where
NZ :: Nat Z
NS :: (S n ~ sn) => Nat n -> Nat sn
data EQ a b = forall q . (a ~ b) => Refl
zerol :: Nat n -> EQ n (Sum Z n)
zerol NZ = Refl
zerol (NS n) = case zerol n of Refl -> Refl
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/1815#changelog
http://ghc.haskell.org/trac/ghc/ticket/1823
http://ghc.haskell.org/trac/ghc/ticket/1823#1823: GADTs and scoped type variables don't work rightFri, 02 Nov 2007 14:09:39 GMTsimonpj<p>
In this program, which is also in the testsuite as <tt>gadt/scoped.hs</tt>, all three definitions of g should work
</p>
<pre class="wiki">{-# OPTIONS_GHC -XGADTs -XScopedTypeVariables -XPatternSignatures #-}
module GADT where
data C x y where
C :: a -> C a a
data D x y where
D :: C b c -> D a c
------- All these should be ok
-- Rejected!
g1 :: forall x y . C x y -> ()
-- C (..) :: C x y
-- Inside match on C, x=y
g1 (C (p :: y)) = ()
-- OK!
g2 :: forall x y . C x y -> ()
-- C (..) :: C x y
-- Inside match on C, x=y
g2 (C (p :: x)) = ()
-- Rejected!
g3 :: forall x y . D x y -> ()
-- D (..) :: D x y
-- C (..) :: C sk y
-- sk = y
-- p :: sk
g3 (D (C (p :: y))) = ()
</pre><p>
But they don't. The reason is that the "refinement" is applied to the environment only after checking an entire pattern; but the refinement is needed during checking the pattern if scoped type variables are to work right.
</p>
<p>
I don't propose to fix this, because it'll come out in the wash when we get rid of type refinements in favour of equality constraints.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1823#changelog
http://ghc.haskell.org/trac/ghc/ticket/1900
http://ghc.haskell.org/trac/ghc/ticket/1900#1900: Type families with class constraints: type-checker loopsThu, 15 Nov 2007 15:02:31 GMTh.holtmann<p>
The following program:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
class (Eq (Depend s))=> Bug s where
type Depend s
trans :: Depend s -> Depend s
instance Bug Int where
type Depend Int = ()
trans = (+1)
check :: (Bug s) => Depend s -> Bool
check d = d == trans d
</pre><p>
runs into a type-checker loop
</p>
<pre class="wiki">GHC-Bug.hs:1:0:
Context reduction stack overflow; size = 20
Use -fcontext-stack=N to increase stack size to N
`ic :: {(Bug Int, Eq (Depend Int)) => Num ()}'
arising from the type signature for `trans' at GHC-Bug.hs:24:2-13
`ic :: {(Bug Int, Eq (Depend Int)) => Num ()}'
arising from the type signature for `trans' at GHC-Bug.hs:24:2-13
<snip>
</pre><p>
Of course, this program should not compile, but the type-checker should not loop.
</p>
<p>
compiler: 6.9.20071105
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/1900#changelog
http://ghc.haskell.org/trac/ghc/ticket/1968
http://ghc.haskell.org/trac/ghc/ticket/1968#1968: data family + GADT: not implemented yetMon, 10 Dec 2007 23:08:33 GMTRemi<p>
My very first attempt at playing with data type families + GADTs went wrong, using 6.9.20071209:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, GADTs #-}
data family HiThere a :: *
data instance HiThere () where
HiThere :: HiThere ()
</pre><pre class="wiki">GHCi, version 6.9.20071209: http://www.haskell.org/ghc/ :? for help
Loading package base ... linking ... done.
[1 of 1] Compiling Main ( bar.hs, interpreted )
*** Exception: typecheck/TcTyClsDecls.lhs:(878,4)-(884,42): Non-exhaustive patterns in function choose_univs
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/1968#changelog
http://ghc.haskell.org/trac/ghc/ticket/2004
http://ghc.haskell.org/trac/ghc/ticket/2004#2004: Pattern matching against GADTs without -XGADTs has odd behavior.Thu, 27 Dec 2007 21:24:08 GMTguest<p>
I'm getting a weird error message declaring a function in GHCi, but the same function declared in the source file works.
</p>
<p>
Repro case:
</p>
<pre class="wiki">{-# LANGUAGE GADTs #-}
module Bug where
data Witness a b c where
Z :: Witness a as (a,as)
P :: Witness a as xs -> Witness a (b,as) (b,xs)
data Expr a vars where
Lam :: String -> Expr a (b,vars) -> Expr (b -> a) vars
Ap :: Expr (b -> a) vars -> Expr b vars -> Expr a vars
subst :: Witness a vs vsa -> Expr a vs -> Expr b vsa -> Expr b vs
subst = undefined
subAp :: Expr a vs -> Expr a vs
subAp (Ap (Lam _ e) v) = subst Z v e
</pre><p>
This compiles fine. But in GHCi:
</p>
<pre class="wiki">> let { subAp2 :: Expr a vs -> Expr a vs ; subAp2 (Ap (Lam _ e) v) = subst Z v e }
<interactive>:1:79:
Couldn't match expected type `a1' against inferred type `a2'
`a1' is a rigid type variable bound by
the type signature for `subAp2' at <interactive>:1:21
`a2' is a rigid type variable bound by
the constructor `Lam' at <interactive>:1:54
Expected type: Expr a1 (Decl b vs)
Inferred type: Expr a2 (Decl b1 vs)
In the third argument of `subst', namely `e'
In the expression: subst Z v e
</pre><p>
Interestingly, if I do <tt>:set -XGADTs</tt> followed by that declaration, it works.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/2004#changelog
http://ghc.haskell.org/trac/ghc/ticket/2040
http://ghc.haskell.org/trac/ghc/ticket/2040#2040: GADT regressionSun, 13 Jan 2008 17:51:42 GMTguest<p>
The following compiles fine in 6.8.1 but does not in later versions of GHC.
</p>
<p>
I'm not sure if this is related to <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/1823" title="bug: GADTs and scoped type variables don't work right (closed: fixed)">#1823</a>, since there type classes are not involved.
</p>
<p>
A workaround is included below.
</p>
<pre class="wiki">{-# OPTIONS_GHC -Wall -fglasgow-exts #-}
module Bug where
data Teq a b where Teq :: Teq a a
class C a b where proof :: Teq a b
data S a = S a
data W b where
-- This would make every version of GHC happy
-- W :: (C a c , c ~ S b) => W a -> W c
W :: C a (S b) => W a -> W (S b)
foo :: W (S ()) -> W (S ()) -> ()
foo (W (_ :: W a1)) (W (_ :: W a2)) =
case proof :: Teq a1 (S ()) of
Teq -> ()
foo2 :: W (S ()) -> W (S ()) -> ()
foo2 (W (_ :: W a1)) (W (_ :: W a2)) =
case proof :: Teq a1 (S ()) of
Teq -> case proof :: Teq a2 (S ()) of
Teq -> ()
</pre><p>
Results:
</p>
<p>
6.8.1 : OK
</p>
<p>
6.8.2 : foo OK, foo2 FAIL
</p>
<pre class="wiki">Bug.hs:23:16:
Could not deduce (C a1 (S ())) from the context ()
arising from a use of `proof' at Bug.hs:23:16-20
</pre><p>
6.9.20080108 : FAIL
</p>
<pre class="wiki">Bug.hs:16:7:
Could not deduce (C a (S ()))
from the context (S () ~ S b1, C a1 (S b1))
arising from a use of `proof' at Bug.hs:16:7-11
Bug.hs:21:7:
Could not deduce (C a (S ()))
from the context (S () ~ S b1, C a1 (S b1))
arising from a use of `proof' at Bug.hs:21:7-11
Bug.hs:22:16:
Could not deduce (C a1 (S ())) from the context (S () ~ a)
arising from a use of `proof' at Bug.hs:22:16-20
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/2040#changelog
http://ghc.haskell.org/trac/ghc/ticket/2141
http://ghc.haskell.org/trac/ghc/ticket/2141#2141: Internal error on invalid record updateFri, 07 Mar 2008 15:51:38 GMTrl<p>
A silly function:
</p>
<pre class="wiki">foo :: () -> ()
foo x = x { foo = 1 }
</pre><p>
6.8.2 says:
</p>
<pre class="wiki">GHC internal error: `foo' is not in scope
In the expression: x {foo = 1}
In the definition of `foo': foo x = x {foo = 1}
</pre><p>
HEAD's message is a bit more illuminating:
</p>
<pre class="wiki">GHC internal error: `foo' is not in scope during type checking, but it passed the renamer
tcg_type_env of environment: []
In the expression: x {foo = 1}
In the definition of `foo': foo x = x {foo = 1}
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/2141#changelog
http://ghc.haskell.org/trac/ghc/ticket/2146
http://ghc.haskell.org/trac/ghc/ticket/2146#2146: Decomposition rule for equalities is too weak in case of higher-kinded type familiesTue, 11 Mar 2008 14:17:05 GMTchak<pre class="wiki">foo :: (F Int a ~ F Int [a]) => a -> [a]
foo = undefined
</pre><p>
gives us
</p>
<pre class="wiki"> Occurs check: cannot construct the infinite type: a = [a]
</pre><p>
but
</p>
<pre class="wiki">foo :: (F Int a ~ F Bool [a]) => a -> [a]
foo = undefined
</pre><p>
doesn't - although both should lead to the same error.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/2146#changelog
http://ghc.haskell.org/trac/ghc/ticket/2157
http://ghc.haskell.org/trac/ghc/ticket/2157#2157: Equality Constraints with Type FamiliesFri, 14 Mar 2008 14:47:15 GMThpacheco<p>
For the implementation of fixpoint recursive definitions for a datatype I have defined the family:
</p>
<pre class="wiki">type family F a :: * -> *
type FList a x = Either () (a,x)
type instance F [a] = FList a
type instance F Int = Either One
</pre><p>
for which we can define functor instances
</p>
<pre class="wiki">instance (Functor (F [a])) where
fmap _ (Left _) = Left ()
fmap f (Right (a,x)) = Right (a,f x)
...
</pre><p>
However, in the definition of recursive patterns over these representation, I need some coercions to hold such as
</p>
<pre class="wiki">F d c ~ F a (c,a)
</pre><p>
but in the current implementation they are evaluated as
</p>
<pre class="wiki">F d ~ F a /\ c ~(c,a)
</pre><p>
what does not express the semantics of "fully parameterized equality" that I was expecting
</p>
<p>
You can find a pratical example in (<a class="ext-link" href="http://groups.google.com/group/fa.haskell/browse_thread/thread/6ea21dcade9e632f/01148521c33ac29a"><span class="icon"></span>my conversions at the haskell-cafe mailing list</a>)
</p>
<p>
In order to avoid this, the family could be redefined as
</p>
<pre class="wiki">type family F a x :: *
type instance F [a] x = Either() (a,x)
type instance F Int x = Either One x
</pre><p>
but this would mean that I cannot define instances for Functor (F a) because not enough parameters passed to F.
</p>
<p>
PS. This might sound more as a feature request than a bug, so sorry if I misplaced this information. I am willing to work on this subject to help supporting my test case.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/2157#changelog
http://ghc.haskell.org/trac/ghc/ticket/2219
http://ghc.haskell.org/trac/ghc/ticket/2219#2219: GADT match fails to refine type variableMon, 14 Apr 2008 07:13:42 GMTdolio<p>
The following code is accepted by the type checker in 6.8.2, but is rejected by a HEAD build, 6.9.20080411:
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators #-}
data Zero
data Succ a
data FZ
data FS fn
data Fin n fn where
FZ :: Fin (Succ n) FZ
FS :: Fin n fn -> Fin (Succ n) (FS fn)
data Nil
data a ::: b
type family Lookup ts fn :: *
type instance Lookup (t ::: ts) FZ = t
type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn
data Tuple n ts where
Nil :: Tuple Zero Nil
(:::) :: t -> Tuple n ts -> Tuple (Succ n) (t ::: ts)
proj :: Fin n fn -> Tuple n ts -> Lookup ts fn
proj FZ (v ::: _) = v
proj (FS fn) (_ ::: vs) = proj fn vs
</pre><p>
The error in question is:
</p>
<pre class="wiki">Bug.hs:25:16:
Occurs check: cannot construct the infinite type:
t = Lookup (t ::: ts) fn
In the pattern: v ::: _
In the definition of `proj': proj FZ (v ::: _) = v
</pre><p>
Which seems to indicate that the pattern match against <tt>FZ</tt> in the first case is failing to refine the type variable <tt>fn</tt> to <tt>FZ</tt>. Reversing the order of the cases yields the same error, so either the match against FS is working correctly, or the type checker thinks that it can solve <tt>Lookup (t ::: ts) fn ~ Lookup ts fn</tt>.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/2219#changelog
http://ghc.haskell.org/trac/ghc/ticket/2275
http://ghc.haskell.org/trac/ghc/ticket/2275#2275: Poor indication of type error locationFri, 09 May 2008 08:41:41 GMTguest<p>
Using {-# OPTIONS_GHC -XArrows -fno-monomorphism-restriction #-}, and Yampa
Starting from line 32, my program contains:
</p>
<pre class="wiki">fireworkSF :: Point2 GL.GLdouble -> Point2 GL.GLdouble -> Object
fireworkSF p0 pFinal = proc _ -> do
rec
position <- (p0 .+^) ^<< integral -< v0
let shouldExplode = position == pFinal
let killReq = if shouldExplode then Event () else noEvent
let spawnReq = if shouldExplode
then Event (Explode pFinal)
else noEvent
returnA -< ObjectOutput {oState = FireworkState position
,oKillReq = killReq
,oSpawnReq = spawnReq}
where
v0 = (pFinal ^-^ p0) ^/ 2
</pre><p>
The type error reports:
</p>
<pre class="wiki">Firework.hs:32:0:
Couldn't match expected type `Point2 GL.GLdouble'
against inferred type `Vector2 GL.GLdouble'
When using functional dependencies to combine
AffineSpace (Point2 a) (Vector2 a) a,
arising from the instance declaration at <no location info>
AffineSpace (Point2 GL.GLdouble) (Point2 GL.GLdouble) a,
arising from a use of `.+^' at Firework.hs:34:16-23
When generalising the type(s) for `fireworkSF'
</pre><p>
Indicating that the bug is something to do with line 34. The actual bug is that the last line of the paste should read:
</p>
<pre class="wiki"> v0 = (pFinal .-. p0) ^/ 2
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/2275#changelog
http://ghc.haskell.org/trac/ghc/ticket/1807
http://ghc.haskell.org/trac/ghc/ticket/1807#1807: type equality coercions not symmetric + order dependentSat, 27 Oct 2007 00:48:03 GMTguest<p>
I'm not entirely sure this is a bug, but it seems pretty weird behaviour:
</p>
<p>
<tt>a ~ b</tt> cannot always be replaced by <tt>b ~ a</tt>
</p>
<p>
<tt>a ~ b, c ~ d</tt> cannot always be replaced by <tt>c ~ d, a ~ b</tt>
</p>
<pre class="wiki">{-# LANGUAGE TypeFamilies, GADTs #-}
module Test where
data List n where
-- Works
--Cons :: (Maybe n ~ n') => List n -> List n'
--Cons :: (Maybe n ~ n', n' ~ Maybe n) => List n -> List n'
-- Fails
Cons :: (n' ~ Maybe n) => List n -> List n'
--Cons :: (n' ~ Maybe n, Maybe n ~ n') => List n -> List n'
class Snoc i where
snoc :: List i -> List (Maybe i)
instance Snoc i => Snoc (Maybe i) where
snoc (Cons xs) = Cons (snoc xs)
</pre><p>
This module compiles fine with both 6.8.0.20071025 and 6.9.20071025 using one of the first two Constructors. With either of the last two constructors both versions say:
</p>
<pre class="wiki"> Could not deduce (Snoc n) from the context ()
arising from a use of `snoc' at Test.hs:17:27-33
Possible fix: add (Snoc n) to the context of the constructor `Cons'
In the first argument of `Cons', namely `(snoc xs)'
In the expression: Cons (snoc xs)
In the definition of `snoc': snoc (Cons xs) = Cons (snoc xs)
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/1807#changelog
http://ghc.haskell.org/trac/ghc/ticket/2231
http://ghc.haskell.org/trac/ghc/ticket/2231#2231: ASSERT failed! file typecheck/TcMType.lhs line 442 t_a7Fa{tv} [tau]Tue, 22 Apr 2008 18:25:05 GMTguest<p>
As discussed this afternoon on #ghc.
</p>
<p>
From the attached tarball, unpack, cd sessions2, ghci Control/Concurrent/Session/Queens.hs, main
</p>
<p>
What should happen is that it prints "False". However, for me it consistently segfaults. GDB reveals things like:
</p>
<pre class="wiki">*Control.Concurrent.Session.Queens> main
Loading package mtl-1.1.0.0 ... linking ... done.
Loading package array-0.1.0.0 ... linking ... done.
Loading package containers-0.1.0.1 ... linking ... done.
Program received signal SIGSEGV, Segmentation fault.
[Switching to Thread 0x41001950 (LWP 26393)]
0x00002b76022eae6b in memcpy () from /lib/libc.so.6
(gdb) bt
#0 0x00002b76022eae6b in memcpy () from /lib/libc.so.6
#1 0x000000000167f7b9 in schedule (initialCapability=<value optimized out>, task=0x1b9d100) at Schedule.c:2847
#2 0x000000000167f94f in workerStart (task=0x1b9d100) at Schedule.c:2528
#3 0x00002b760205e017 in start_thread () from /lib/libpthread.so.0
#4 0x00002b76023385bd in clone () from /lib/libc.so.6
#5 0x0000000000000000 in ?? ()
</pre><p>
For some people, the first time you run main, it doesn't segfault but also doesn't print anything. Then the second time you run main, it will segfault then.
</p>
<p>
Compiling with ghc does result in the right (non-segfaulting) behaviour, both with -threaded and without.
</p>
<p>
For me, this is with 6.8.2, but Igloo confirmed that it segfaults HEAD too.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/2231#changelog