GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=!closed&owner=diatchki&order=type
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?status=!closed&owner=diatchki&order=type
Trac 1.0.1
http://ghc.haskell.org/trac/ghc/ticket/8178
http://ghc.haskell.org/trac/ghc/ticket/8178#8178: Need TypeRep for Symbol and numeric type literals; and Typeable instancesTue, 27 Aug 2013 11:45:28 GMTsimonpj<p>
Nicolas Trangez points out that we don't have a <tt>TypeRep</tt> for types involving literal strings or numerics. E.g. what is <tt>(typeRep (undefined :: Proxy "foo"))</tt>?
</p>
<p>
Here is Nicolas's example:
</p>
<pre class="wiki">{-# LANGUAGE DataKinds,
KindSignatures,
DeriveFunctor,
DeriveDataTypeable #-}
module Main where
import Data.Typeable
import GHC.TypeLits
data NoSymbol n a b = NoSymbol a b
deriving (Typeable)
data WithSymbol (n :: Symbol) a b = WithSymbol a b
deriving (Typeable)
data Sym
deriving (Typeable)
main :: IO ()
main = do
print $ typeOf (undefined :: NoSymbol Sym Int Int)
let d = undefined :: WithSymbol "sym" Int Int
{-
print $ typeOf d
No instance for (Typeable Symbol "sym")
arising from a use of ‛typeOf’
-}
return ()
</pre><p>
Just as types contain literal strings and natural numbers, so too must <tt>TypeRep</tt>, in some way. Once we have a suitable <tt>TypeRep</tt> we can make built-in instance for <tt>Typeable</tt> that return the appropriate representation.
</p>
<p>
At the moment we have (in <tt>Data.Typeable.Internals</tt>):
</p>
<pre class="wiki">data TypeRep = TypeRep {-# UNPACK #-} !Fingerprint TyCon [TypeRep]
data TyCon = TyCon {
tyConHash :: {-# UNPACK #-} !Fingerprint,
tyConPackage :: String,
tyConModule :: String,
tyConName :: String
}
</pre><p>
with instances for Eq and Ord. Perhaps we need
</p>
<pre class="wiki">data TypeRep
= TcApp {-# UNPACK #-} !Fingerprint TyCon [TypeRep]
| TcSym String
| TcNat Integer
</pre><p>
or something like that? I'm not certain. I think Iavor is going to think about it.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/8178#changelog
http://ghc.haskell.org/trac/ghc/ticket/9260
http://ghc.haskell.org/trac/ghc/ticket/9260#9260: Unnecessary error using GHC.TypeLitsThu, 03 Jul 2014 08:08:47 GMTIceland_jack<p>
Compiling:
</p>
<pre class="wiki">{-# LANGUAGE DataKinds, TypeOperators, GADTs #-}
module Error where
import GHC.TypeLits
data Fin n where
Fzero :: Fin (n + 1)
Fsucc :: Fin n -> Fin (n + 1)
test :: Fin 1
test = Fsucc Fzero
</pre><p>
gives a strange (unnecessary) error message claiming that <tt>Fin 1</tt> doesn't match the expected type <tt>Fin (0 + 1)</tt>:
</p>
<pre class="wiki">% ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.8.2
% ghc -ignore-dot-ghci /tmp/Error.hs
[1 of 1] Compiling Error ( /tmp/Error.hs, /tmp/Error.o )
/tmp/Error.hs:12:8:
Couldn't match type ‘0’ with ‘1’
Expected type: Fin 1
Actual type: Fin (0 + 1)
In the expression: Fsucc Fzero
In an equation for ‘test’: test = Fsucc Fzero
/tmp/Error.hs:12:14:
Couldn't match type ‘1’ with ‘0’
Expected type: Fin 0
Actual type: Fin (0 + 1)
In the first argument of ‘Fsucc’, namely ‘Fzero’
In the expression: Fsucc Fzero
%
</pre>Resultshttp://ghc.haskell.org/trac/ghc/ticket/9260#changelog
http://ghc.haskell.org/trac/ghc/ticket/9708
http://ghc.haskell.org/trac/ghc/ticket/9708#9708: Type inference non-determinism due to improvementTue, 21 Oct 2014 13:43:54 GMTsimonpj<p>
Here's an example that showed up in Iavor's test <tt>TcTypeNatSimple</tt>:
</p>
<pre class="wiki"> ti7 :: (x <= y, y <= x) => Proxy (SomeFun x) -> Proxy y -> ()
ti7 _ _ = ()
</pre><p>
From the ambiguity check for <tt>ti7</tt> we get this constraint
</p>
<pre class="wiki"> forall x y. (x <= y, y <= x)
=> ( SomeFun x ~ SomeFun alpha
, alpha <= y, y <= alpha)
</pre><p>
where <tt>alpha</tt> is the unification variable that instantiates <tt>x</tt>.
</p>
<p>
Now, from the givens, improvement gives a derived <tt>[D] x~y</tt>, but we can't actually use that to rewrite anything; we have no evidence.
</p>
<p>
From the wanteds we can use improvement in two alternative ways:
</p>
<pre class="wiki">1. (alpha <= y, y <= alpha) => [D] alpha ~ y
2. (x <= y, y <= alpha) => [D] x <= alpha
(alpha <= y, y <= x) => [D] alpha <= x
And combining the latter two we get [D] (alpha ~ x)
</pre><p>
It is (2) that we want. But if we get (1) and fix <tt>alpha := y</tt>, we get an error <tt>Can't unify (SomeFun x ~ SomeFun y)</tt>.
</p>
<p>
I think it's a fluke that this test has been working so far; in my new flatten-skolem work it has started failing, which is not unreasonable. What I HATE is that whether type checking succeeds or fails depends on some random choice about which constraint is processed first.
</p>
<p>
The real bug is that the derived Given has no evidence, and can't be used for rewriting. I think Iavor is fixing this deficiency for. I speculate that the same problem might also show up with ordinary type-class functional dependencies, but I have not found a concrete example.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/9708#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, BlueSpec, 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/9334
http://ghc.haskell.org/trac/ghc/ticket/9334#9334: Implement "instance chains"Sat, 19 Jul 2014 21:10:04 GMTdiatchki<p>
It would be useful to implement a version of "instance chains" <a class="missing changeset" title="No changeset 1 in the repository">[1]</a> in GHC, which would eliminate the need for OVERLAPPING_INSTANCES in most (all practcial?) programs.
</p>
<p>
The idea is that programmers can explicitly group and order instances into an "instance chain". For example:
</p>
<pre class="wiki">instance (Monad m) => StateM (StateT s m) s where ...
else (MonadTrans t, StateM m s) => StateM (t m) s where ...
</pre><p>
When GHC searches for instances, the instances in a chain are considered together and in order, starting with the first one:
</p>
<ol><li>If the goal matches the current instance's head, then this instance is selected and the rest are ignored, as if they were not there;
</li></ol><ol start="2"><li>If the goal does not match the current instance's head, AND it does not unify with the current instance's head, then we skip the instance and proceed to the next member of the chain;
</li></ol><ol start="3"><li>If the goal does not match the current instance's head, but it does unify with it, then we cannot use this chain to solve the goal.
</li></ol><p>
In summary: earlier instances in a chain "hide" later instances, and later instances can be reached only if we are sure that none of the previous instance will match.
</p>
<p>
<a class="missing changeset" title="No changeset 1 in the repository">[1]</a> <a class="ext-link" href="http://web.cecs.pdx.edu/~mpj/pubs/instancechains.pdf"><span class="icon"></span>http://web.cecs.pdx.edu/~mpj/pubs/instancechains.pdf</a>
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/9334#changelog