#7730: :info and polykinds
--------------------------------------------+------------------------------
Reporter: monoidal | Owner: archblob
Type: bug | Status: new
Priority: normal | Milestone: 7.10.1
Component: Compiler (Type checker) | Version: 7.6.2
Resolution: | Keywords:
Operating System: Unknown/Multiple | Architecture:
Type of failure: None/Unknown | Unknown/Multiple
Test Case: | Difficulty: Unknown
Blocking: | Blocked By:
| Related Tickets: #8776
--------------------------------------------+------------------------------
Comment (by archblob):
I have added a working, validated patch. It can be reviewed and I'll make
the necessary modification if all is not well. Otherwise I think it can be
merged and I've also added tests.
It does not include the fix for {{{:kind}}} because I thought it would be
best to separate them. I will include another patch for that after we are
done with this one.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/7730#comment:42>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#8673: GHC could generate GADT record selectors in more cases
------------------------------------+-------------------------------------
Reporter: simonpj | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.3
Keywords: | Operating System: Unknown/Multiple
Architecture: Unknown/Multiple | Type of failure: None/Unknown
Difficulty: Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: |
------------------------------------+-------------------------------------
Philip Holzenspies writes (in email to ghc-users):
I was playing around with GADT-records again and ran into behaviour that
I'm not sure is intentional. Given this program:
{{{
{-#LANGUAGE GADTs #-}
data FooBar x a where
Foo :: { fooBar :: a } -> FooBar Char a
Bar :: { fooBar :: a } -> FooBar Bool a
}}}
GHC tells me this:
{{{
foo.hs:3:1:
Constructors Foo and Bar have a common field `fooBar',
but have different result types
In the data declaration for `FooBar'
Failed, modules loaded: none.
}}}
The user guide does say (section 7.4.7): "However, for GADTs there is
the following additional constraint: every constructor that has a field
f must have the same result type (modulo alpha conversion)." So this
behaviour is documented in the user guide. However, it seems reasonable
that in the case above, where all the relevant variables are exposed in
the result type of both constructors, this should be perfectly typeable.
In other words, shouldn't GHC be able to derive a type that is simply:
{{{
fooBar :: FooBar x a -> a
}}}
?
Is this something that was simply never implemented, but could be, or is
this not decidable or prohibitively computationally complex?
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8673>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9108: GADTs and pattern type annotations?
------------------------------------+-------------------------------------
Reporter: edsko | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.8.2
Keywords: | Operating System: Unknown/Multiple
Architecture: Unknown/Multiple | Type of failure: None/Unknown
Difficulty: Unknown | Test Case:
Blocked By: | Blocking:
Related Tickets: |
------------------------------------+-------------------------------------
Consider
{{{
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Data.Tagged
data Sing (xs :: [k]) where
SNil :: Sing '[]
SCons :: SingI xs => Sing (x ': xs)
class SingI (a :: [k]) where
sing :: Sing a
instance SingI '[] where
sing = SNil
instance SingI xs => SingI (x ': xs) where
sing = SCons
lengthSing :: forall (xs :: [k]). SingI xs => Tagged xs Int
lengthSing = case sing :: Sing xs of
SNil -> Tagged 0
(SCons :: Sing (x ': xs')) -> Tagged (1 + untag (lengthSing :: Tagged
xs' Int))
}}}
This gives a type error:
{{{
Could not deduce (xs ~ (x : xs'))
from the context (SingI xs)
bound by the type signature for
lengthSing :: SingI xs => Tagged xs Int
at Bug.hs:23:15-59
‘xs’ is a rigid type variable bound by
the type signature for lengthSing :: SingI xs => Tagged xs Int
at Bug.hs:23:22
Expected type: Sing xs
Actual type: Sing (x : xs')
}}}
But once we pattern match on the `SCons` we know that `xs ~ x ': xs'` for
some `x`, `xs'`, and we should be able to bring them into scope.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9108>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#6018: Injective type families
-------------------------------+-------------------------------------------
Reporter: lunaris | Owner: simonpj
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies, Injective
Resolution: | Architecture: Unknown/Multiple
Operating System: | Difficulty: Unknown
Unknown/Multiple | Blocked By:
Type of failure: | Related Tickets: #4259
None/Unknown |
Test Case: |
Blocking: |
-------------------------------+-------------------------------------------
Comment (by spacekitteh):
Here's another real world use case.
Given
{{{
class Manifold' a where
type Field a
type Base a
type Tangent a
type TangentBundle a
type Dimension a∷ Nat
type UsesMetric a∷ Symbol
project ∷ a → Base a
unproject ∷ Base a→ a
tangent ∷ a → TangentBundle a
cotangent ∷ a → (TangentBundle a→ Field a)
}}}
then this works:
{{{
id' ∷ ∀ a. ( Manifold' a) ⇒ Base a → Base a
id' input= project out where
out∷a
out = unproject input
}}}
whereas this requires injective type families:
{{{
id' ∷ ∀ a. ( Manifold' a) ⇒ Base a → Base a
id' = project ∘ unproject
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:26>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9093: Type synonym accepted with out-of-scope kind variable
--------------------------+------------------------------------------------
Reporter: | Owner:
goldfire | Status: new
Type: bug | Milestone:
Priority: normal | Version: 7.8.2
Component: | Operating System: Unknown/Multiple
Compiler | Type of failure: GHC accepts invalid program
Keywords: | Test Case:
Architecture: | Blocking:
Unknown/Multiple |
Difficulty: |
Unknown |
Blocked By: |
Related Tickets: |
--------------------------+------------------------------------------------
When I say
{{{
{-# LANGUAGE PolyKinds #-}
import Data.Proxy
import GHC.Exts
type X = Proxy (Any :: k)
}}}
I get no error. If I then ask GHCi about `X` (with `-fprint-explicit-
kinds`), I see this:
{{{
*Main> :i X
type X = Proxy AnyK (Any AnyK)
}}}
I think my original code should be rejected.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9093>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9107: An alternative to witness values
----------------------------------------------+----------------------------
Reporter: spacekitteh | Owner:
Type: feature request | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.9
Keywords: | Operating System:
Architecture: Unknown/Multiple | Unknown/Multiple
Difficulty: Moderate (less than a day) | Type of failure:
Blocked By: | None/Unknown
Related Tickets: | Test Case:
| Blocking:
----------------------------------------------+----------------------------
So, I might have come up with a nicer notation to providing type
witnesses.
Say I have a class thusly:
{{{
class Metric a where
measure :: Vector f -> Vector f -> f
}}}
and an example instance:
{{{
instance Metric "Euclidean" where
measure = sum . (zipWith (*))
}}}
In order to actually use a specific metric, one would have to modify the
type signature to include a witness, and use it such as {{{measure
undefined::"Euclidean" a b}}}. Personally, I find such expressions to be
ugly clutter.
Instead, here are three alternate proposals which don't require including
a witness:
1. {{{(Metric "Euclidean") => <term involving measure>}}} for example
{{{dot a b = (Metric "Euclidean") => measure a b}}}
2. New keyword similar to "where"
{{{
dot a b = measure a b assuming (Metric "Euclidean")
}}}
3. New keyword similar to "let..in"
{{{dot a b = assume (Metric "Euclidean") in measure a b}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9107>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
