Rafaël Bocquet

Issue with HIT path constructors.

3

This is probably roughly the same bug as #35, but as it does not involve recursive HITs, I am creating a separate issue. It is possible to create a path...

Self quantification in data declarations

2

Currently, this declaration : ``` haskell data A :: * where B :: forall (x :: A). A ``` results in a "AThing evaluated unexpectedly" ghc panic. I think it...

Kind unification error (or unhelpful error message ?)

4

It seems in this case that ghc is able to check `t : k1` and `t : k2`, but fails to unify k1 with k2 (`t=AH t t6 t2 t7...

This is the code from #38, with a typed hole instead of the expression causing the error. ``` haskell {-# LANGUAGE GADTs, RankNTypes, DataKinds, PolyKinds, TypeFamilies, TypeOperators, ScopedTypeVariables #-} {-#...

Here is an example hanging the compiler : ``` haskell {-# LANGUAGE GADTs, TypeFamilies, TypeOperators, DataKinds, PolyKinds, RankNTypes, ScopedTypeVariables #-} module A where data N = Z | S N...

Error with multiple constructors

1

I played a bit with this branch of ghc, and got this strange error : ``` haskell {-# LANGUAGE GADTs, TypeFamilies, TypeOperators, DataKinds, PolyKinds, RankNTypes, ScopedTypeVariables #-} module A where...

The following code ```ocaml let () = let arr : Int32.t CCVector.vector = CCVector.create () in CCVector.push arr (Int32.of_int 123456); Format.printf "%d\n" (Int32.to_int (CCVector.get arr 0)); let x = CCVector.get...