#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature request | Status: new
Priority: normal | Milestone: 7.12.1
Component: Compiler | Version: 7.4.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | TypeFamilies, Injective
Type of failure: None/Unknown | Architecture:
Blocked By: | Unknown/Multiple
Related Tickets: #4259 | Test Case:
| Blocking:
| Differential Revisions: Phab:D202
-------------------------------------+-------------------------------------
Comment (by jstolarek):
Replying to [comment:103 jberryman]:
> I've only had use for better type inference with (conceptually) closed,
recursive type families
Calling type families from an injective type family will not be allowed
(including recursion). The reason is that I don't see a way of verifying
injectivity when type families are involved.
> What I think I want is something like proposal C from the wiki
At the moment I am implementing proposals A and B. C is something to think
about in the future, as it is not trivial.
> And as a naive user I want injectivity to be inferred for closed type
families, and don't find the arguments against it in the wiki convincing.
Yes, I suppose that focus of the wiki discussion is a bit off. I think we
could infer injectivity of type A for closed type families. But I don't
think we should try to infer injectivity of type B because the algorithm
is exponential - see [comment:64 comment 64]. That's the major reason for
doing this. (Numbers in that comment were computed for type C injectivity,
but type B is also exponential.)
{{{#!hs
-- | The algebraic normal form 'Exponent' @abc@ distributed over the
single
-- base variable @x@.
type family abc :=>-> x
-- | x¹ = x
type instance () :=>-> x = x
-- | x⁽ᵃᵇ⁾ = (xᵇ)ᵃ
type instance (a,bs) :=>-> x = a -> bs :=>-> x
}}}
I don't think `:=>->` type family is injective: both `() :=>-> (Int ->
Int)` and `(Int,()) :=>-> Int` reduce to `Int -> Int`.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:104>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature request | Status: new
Priority: normal | Milestone: 7.12.1
Component: Compiler | Version: 7.4.1
Resolution: | Keywords:
Operating System: Unknown/Multiple | TypeFamilies, Injective
Type of failure: None/Unknown | Architecture:
Blocked By: | Unknown/Multiple
Related Tickets: #4259 | Test Case:
| Blocking:
| Differential Revisions: Phab:D202
-------------------------------------+-------------------------------------
Comment (by jberryman):
I'm very late to the discussion, so this is probably not helpful at all,
but I wanted to mention my interest. I've only had use for better type
inference with (conceptually) closed, recursive type families. What I
think I want is something like proposal C from the wiki, or the head-
injectivity proposal where "possibly-partial information about the result
might allow us to deduce possibly-partial information about the
arguments."
And as a naive user I want injectivity to be inferred for closed type
families, and don't find the arguments against it in the wiki convincing.
Intuitively there doesn't seem to be much difference between the level of
logic required to infer things about types with closed type synonym
families, vs the sort of inference the typechecker does elsewhere (again,
as a naive user who doesn't care about the trickiness of implementing such
a scheme). My impression is that this is what many people assumed would be
the point of closed type families; for what I've had in mind closed type
families make only a cosmetic improvement.
Anyway most of my interest came from my work on
https://github.com/jberryman/shapely-data which embarrassingly seems to
dependent quite a lot on #1241, so it (and below) needs GHC 7.6. You can
ignore the example that follows or consider it if it's helpful:
{{{#!hs
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-} -- for nested Type family: Reversed
(Tail t) :> Head t
{-# LANGUAGE FunctionalDependencies #-}
-- | A class for the exponent laws with the 'Normal' form @abc@ in the
exponent
-- place. See the instance documentation for concrete types and examples.
class Exponent abc where
fanin :: (abc :=>-> x) -> (abc -> x)
unfanin :: (abc -> x) -> (abc :=>-> x)
-- | The algebraic normal form 'Exponent' @abc@ distributed over the
single
-- base variable @x@.
type family abc :=>-> x
-- | x¹ = x
type instance () :=>-> x = x
-- | x⁽ᵃᵇ⁾ = (xᵇ)ᵃ
type instance (a,bs) :=>-> x = a -> bs :=>-> x
instance Exponent () where
fanin = const
unfanin f = f ()
instance (Exponent bs)=> Exponent (a,bs) where
fanin f = uncurry (fanin . f)
unfanin f = unfanin . curry f
class Homogeneous a as | as -> a where
-- An n-ary @codiag@.
genericRepeat :: a -> as
instance Homogeneous a () where
genericRepeat _ = ()
instance (Homogeneous a as)=> Homogeneous a (a,as) where
genericRepeat a = (a,genericRepeat a)
}}}
So the following two type-check fine:
{{{#!hs
a = (3 ==) $ (\(x,(y,(z,())))-> x+y+z) $ genericRepeat 1
b = (3 ==) $ fanin (\x y z-> x+y+z) (genericRepeat 1 ::
(Int,(Int,(Int,()))))
}}}
But this doesn't:
{{{#!hs
c = (3 ==) $ fanin (\x y z-> x+y+z) $ genericRepeat 1
}}}
...failing with
{{{
Couldn't match expected type `a1 -> a1 -> a1 -> a1'
with actual type `abc0 :=>-> a0'
The type variables `a0', `abc0', `a1' are ambiguous
Possible fix: add a type signature that fixes these type variable(s)
The lambda expression `\ x y z -> x + y + z' has three arguments,
but its type `abc0 :=>-> a0' has none
In the first argument of `fanin', namely `(\ x y z -> x + y + z)'
In the expression: fanin (\ x y z -> x + y + z)
}}}
That library is probably going in the garbage bin at this point, but in
general this is the sort of thing I think I'd like to be able to do with
type families eventually. And I haven't gotten to dig into y'all's
singletons work yet, so it might be that that's the sort of thing I'm
looking for and my use of type families and classes in shapely-data is
ill-considered.
Thanks for your work on this!
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:103>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9973: Erroneous Redundant constraint warning
-------------------------------------+-------------------------------------
Reporter: alanz | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.11
Keywords: | Operating System: Unknown/Multiple
Architecture: | Type of failure: None/Unknown
Unknown/Multiple | Blocked By:
Test Case: | Related Tickets:
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Using version 4425ab99d6410839fa7567950b0a4696b0a3d70f with D538 applied,
If the attached source file is loaded as is into ghci it generates the
following warning for line 5, but otherwise loads fine
{{{
/home/alanz/mysrc/github/alanz/HaRe/Bug2.hs:5:18: Warning:
Redundant constraint: SYB.Data t
In the type signature for:
duplicateDecl :: SYB.Data t =>
[GHC.LHsBind GHC.Name]
-> t -> GHC.Name -> GHC.Name -> IO [GHC.LHsBind
GHC.Name]
}}}
If the constraint is commented out, it results in an error
{{{
/home/alanz/mysrc/github/alanz/HaRe/Bug2.hs:26:16:
No instance for (SYB.Data t)
arising from a use of ‘definingSigsNames’
Possible fix:
add (SYB.Data t) to the context of
the type signature for:
duplicateDecl :: [GHC.LHsBind GHC.Name]
-> t -> GHC.Name -> GHC.Name -> IO [GHC.LHsBind
GHC.Name]
In the expression: definingSigsNames [n] sigs
In an equation for ‘typeSig’: typeSig = definingSigsNames [n] sigs
In an equation for ‘duplicateDecl’:
duplicateDecl decls sigs n newFunName
= do { let sspan = ...;
newSpan <- case typeSig of {
[] -> return sspan
_ -> ... };
let rowOffset = ...;
.... }
where
typeSig = definingSigsNames [n] sigs
Failed, modules loaded: none.
}}}
This behaviour goes away if the following lines are commented out
{{{#!hs
let rowOffset = case typeSig of
[] -> 2
_ -> 1
}}}
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9973>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9875: ld -l:filename.dylib does not appear to be portable
------------------------------------+-------------------------------------
Reporter: ezyang | Owner:
Type: bug | Status: new
Priority: high | Milestone: 7.10.1
Component: GHCi | Version: 7.9
Keywords: | Operating System: MacOS X
Architecture: Unknown/Multiple | Type of failure: GHCi crash
Difficulty: Unknown | Test Case: T2276_ghci
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
------------------------------------+-------------------------------------
In GHCi, we seem to use `-l:` to ask the linker to link a specific
filename, instead of munging the filename. Unfortunately, this does not
appear to be universally supported by all versions of `ld`. Here is the
manpage `ld` that comes with Mac OS X 10.10.1:
{{{
Options that control libraries
-lx This option tells the linker to search for libx.dylib or
libx.a in
the library search path. If string x is of the form y.o,
then that
file is searched for in the same places, but without
prepending
`lib' or appending `.a' or `.dylib' to the filename.
}}}
It causes T2276_ghci to fail:
{{{
--- /dev/null 2014-12-09 20:57:29.000000000 -0500
+++ ./T2276_ghci.run.stderr 2014-12-09 20:57:30.000000000 -0500
@@ -0,0 +1,3 @@
+ld: library not found for -l:ghc75404_1.dylib
+clang: error: linker command failed with exit code 1 (use -v to see
invocation)
+phase `Linker' failed (exitcode = 1)
*** unexpected failure for T2276_ghci(ghci
}}}
Regression seems to have been introduced by:
{{{
commit 383733b9191a36e2d3f757700842dbc3855911d9
Author: Peter Trommler <ptrommler(a)acm.org>
Date: Sun Nov 30 12:00:39 2014 -0600
Fix obscure problem with using the system linker (#8935)
}}}
Probably we can fix it by not using colon and making sure the libraries we
generate have the right file format.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9875>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9967: Pattern synonym type signature documentation out of date
-------------------------------------+-------------------------------------
Reporter: goldfire | Owner:
Type: bug | Status: new
Priority: normal | Milestone: 7.10.1
Component: | Version: 7.10.1-rc1
Documentation | Operating System: Unknown/Multiple
Keywords: | Type of failure: None/Unknown
Architecture: | Blocked By:
Unknown/Multiple | Related Tickets:
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Section 7.3.9.3 of the 7.10.1 RC1 user's guide uses the old pattern
synonym type syntax for `ExNumPat`. I'd fix it myself, but I'm not 100%
sure I'd do it correctly.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9967>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9934: Typo in GHC.RTS.Flags
-------------------------------------+-------------------------------------
Reporter: RyanGlScott | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: libraries/base | Version: 7.10.1-rc1
Keywords: | Operating System:
Architecture: Unknown/Multiple | Unknown/Multiple
Difficulty: Easy (less than 1 | Type of failure: Other
hour) | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
-------------------------------------+-------------------------------------
Currently, the {{{GCFlags}}} data type in the {{{GHC.RTS.Flags}}} module
of {{{base-4.8.0.0}}} has a field named {{{heapSizeSuggesionAuto}}}
(without a {{{t}}} in {{{Suggesion}}}). Given that the corresponding
struct field in {{{rts/Flags.h}}} is named {{{heapSizeSuggestionAuto}}},
this is probably a typo.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9934>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
