GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=!closed&reporter=diatchki&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&reporter=diatchki&order=id
Trac 1.0.1
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/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/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