#8025: "During interactive linking, GHCi couldn't find the following symbol"
typechecker error with TemplateHaskell involved
-------------------------------------+-------------------------------------
Reporter: mojojojo | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Compiler | Version: 7.6.3
(Type checker) | Keywords:
Resolution: | Architecture: x86
Operating System: MacOS X | Difficulty: Unknown
Type of failure: Incorrect | Blocked By:
warning at compile-time | Related Tickets:
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by GregWeber):
This issue is being seen while running: cabal install yesod-core
https://github.com/yesodweb/yesod/issues/721
I am using ghc 7.8.3 on Ubuntu linux from this Dockerfile: zsol/haskell-
platform-2014.2.0.0
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8025#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#5793: make nofib awesome
-------------------------------------+-------------------------------------
Reporter: dterei | Owner: dterei
Type: task | Status: new
Priority: normal | Milestone: ⊥
Component: NoFib | Version:
benchmark suite | Keywords:
Resolution: | Architecture: Unknown/Multiple
Operating System: | Difficulty: Unknown
Unknown/Multiple | Blocked By: 9571
Type of failure: | Related Tickets:
None/Unknown |
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by NeilMitchell):
Reflecting on why this ticket didn't go anywhere, perhaps the scope is too
broad. Rather than "make nofib awesome" maybe we need a few separate
tickets - the one to switch nofib to Shake just requires integrating the
code that is already written. The other issues such as
criterion/stabilizer and changing the set of benchmarks might do best
being tackled as individual pieces.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5793#comment:32>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9680: Autogenerated lib/include/HsTimeConfig.h is checked in
-------------------------------------+-------------------------------------
Reporter: gintas | Owner:
Type: bug | Status: new
Priority: low | Milestone:
Component: Build System | Version: 7.9
Keywords: | Operating System: Windows
Architecture: Unknown/Multiple | Type of failure:
Difficulty: Easy (less than 1 | None/Unknown
hour) | Test Case:
Blocked By: | Blocking:
Related Tickets: | Differential Revisions:
-------------------------------------+-------------------------------------
lib/include/HsTimeConfig.h appears to be generated by the build process,
but it's checked into the depot. After I run make it shows up as modified
under git status, preventing "arc diff" etc.
I am building on Windows, but I don't think this is OS-specific.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9680>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#9604: Python test runner assumes native Python on Windows
-------------------------------------+-------------------------------------
Reporter: gintas | Owner:
Type: bug | Status: new
Priority: normal | Milestone:
Component: Build System | Version: 7.8.2
Keywords: | Operating System: Windows
Architecture: Unknown/Multiple | Type of failure: Building
Difficulty: Unknown | GHC failed
Blocked By: | Test Case:
Related Tickets: | Blocking:
| Differential Revisions:
-------------------------------------+-------------------------------------
runtests.py assumes that ctypes.windll is always available when running on
Windows, but that is in fact only available when using a native Windows
Python, but not the mingw/msys Python. The code causes a crash over a
trivial issue of setting the terminal to UTF-8 mode.
See attached patch for a fix. (The second patch is a cleanup.)
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9604>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies,
Resolution: | Injective
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets: #4259
Test Case: |
Blocking: |
Differential Revisions: Phab:D202 |
-------------------------------------+-------------------------------------
Comment (by jstolarek):
Replying to [comment:79 goldfire]:
> I'm ambivalent on this design decision (that the variables have to be in
the same order in the annotation). I suppose it simplifies the
implementation.
I guess my argument about simpler implementation is not that important. I
mean the code is quite simple in both cases. It's more like a choice
between linear and quadratic algorithm. I'd went for linear, even if it
adds an extra restriction on the user code.
> Yes, Simon's comment above is correct -- I was just wrong about the
`isDecomposableTyCon` thing.
OK. Reverting :-)
> What works perfectly fine? Not the code you wrote above, because it
contains a not-currently-parsed injectivity annotation. I tried it without
the injectivity annotation, and it does indeed work.
Yes, that's what I meant.
> But not because of injectivity, at all: it's because GHC is clever
enough to figure out that `F` is just an identity function
Right. Still, I wondering how this works. I mean there are probably no
special cases in the typechecker that try to guess whether a type family
is an identity function?
> Fair warning: 1000 lines of `-ddump-tc-trace` isn't long at all! :)
I imagine, given that my source file was 8 lines of code. Still, it's a
bit steep learning curve.
Replying to [comment:80 goldfire]:
> Under the singletons work, we gave a different kind to non-injective
functions
Ah, right.
Replying to [wiki:InjectiveTypeFamilies wiki comments]:
> I believe this would also have to check that all variables mentioned in
the LHS are mentioned in the RHS. Or, following along with Simon's idea in
comment:76:ticket:6018, those variables that appear in the injectivity
annotation must be mentioned in the RHS.
I haven't thought about that. I believe you're right.
> We have to be careful with the word overlap here. I think we want
"overlaps" to be "is subsumed by".
I don't see the difference between "overlaps" and "is subsumed by". :-(
Now, in 4c I wrote:
> if unification [of the RHSs] succeeds and there are type variables
involved we substitute unified type variables on the LHS and check whether
this LHS overlaps with any of the previous equations. If it does we
proceed to the next equation
You replied with this:
> you want to know of the equation at hand is reachable, given the LHS
substitution. Even if it is reachable, the (substituted) LHS may coincide
with the LHS of the earlier equation whose RHS unified with the current
RHS.
I don't see the difference between your version and mine.
> Even subtler, it's possible that certain values for type variables are
excluded if the current LHS is reachable (for example, some variable a
couldn't be Int, because if a were Int, then a previous equation would
have triggered). Perhaps these exclusions can also be taken into account.
Hm... can you give an example where this would be useful?
> '''RAE:''' But it seems that, under this treatment, any self-recursion
would automatically lead to a conclusion of "not injective", just like any
other use of a type family. For example:
>
> {{{#!hs
> type family IdNat n where
> IdNat Z = Z
> IdNat (S n) = S (IdNat n)
> }}}
>
> `IdNat` is injective. But, following the algorithm above, GHC would see
the recursive use of `IdNat`, not know whether `IdNat` is injective, and
then give up, concluding "not injective". Is there a case where the
special treatment of self-recursion leads to a conclusion of "injective"?
'''End RAE'''
This example is just like my `NatToMaybe`. My idea here was that RHSs of
these two equations won't unify - first returns `Z`, second returns `S
something`. These are distinct constructors that have no chance of being
unified. (I assumed that we are able to detect that.) There are no calls
to type families other than self-recursion and so we can declare `IdNat`
to be injective. I admit I am not 100% certain that allowing self-
recursion is safe. It's just that I was unable to come up with an example
that would show that my algorithm: a:) declares injective function to be
non-injective; b) declares a non-injective function to be injective.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:82>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#5793: make nofib awesome
-------------------------------------+-------------------------------------
Reporter: dterei | Owner: dterei
Type: task | Status: new
Priority: normal | Milestone: ⊥
Component: NoFib | Version:
benchmark suite | Keywords:
Resolution: | Architecture: Unknown/Multiple
Operating System: | Difficulty: Unknown
Unknown/Multiple | Blocked By: 9571
Type of failure: | Related Tickets:
None/Unknown |
Test Case: |
Blocking: |
Differential Revisions: |
-------------------------------------+-------------------------------------
Comment (by rwbarton):
We should consider incorporating something along the lines of
[https://github.com/ccurtsinger/stabilizer Stabilizer] in order to reduce
the magnitude of the effects seen in #8279.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/5793#comment:30>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies,
Resolution: | Injective
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets: #4259
Test Case: |
Blocking: |
Differential Revisions: Phab:D202 |
-------------------------------------+-------------------------------------
Comment (by goldfire):
Replying to [comment:76 simonpj]:
> * My brain is too small to think about verifying injectivity for closed
families. Richard?
I've put some comments on the wiki page. But the whole thing makes me a
little nervous, as closed type families are really squirrelly. I would
want something resembling a proof before feeling truly confident. As a
first pass, we could always treat the equations of a closed family as
independent (like an open family). I believe that such a treatment would
be fully conservative.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:81>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies,
Resolution: | Injective
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets: #4259
Test Case: |
Blocking: |
Differential Revisions: Phab:D202 |
-------------------------------------+-------------------------------------
Comment (by goldfire):
Replying to [comment:75 jstolarek]:
> Good question. I have not considered such case earlier. Here are some
thoughts:
>
> Currently your `Map` function will work only for type constructors
because unsaturated type families are not allowed. These are certainly
injective.
>
> First step in my current outline of the algorithm that decides whether a
type family is injective or not says: "If a RHS contains a call to a type
family we conclude that the type family is not injective. I am not certain
if this extends to self-recursion -- see discussion below." This would
lead to conclusion that `Map` is not injective because `Map` calls itself.
>
> Now let's say I manage to find a way to allow self-recursion (see
discussion on the wiki page). I'm left with the problematic call to `f`.
As stated earlier currently this must be an injective type constructor. So
it seems that declaring `Map` injective should be safe because type
constructors are generative and it seems possible to deduce `f`, `a` and
`b` from `Map f [a, b] ~ [Maybe Int, Maybe Char]`. At the moment I have no
idea how to formulate an algorithm for such a deduction. Could this be
done by the current constraint solver?
This should just work with the algorithm already stated. (Except for the
self-recursion bit, which I responded to on the wiki page.) Unification
should do the work for you.
>
> What if we were allowed to have partially applied type families (say,
because we've implemented ideas from singletons) and `f` could be a type
family? Would knowing that `f` is injective allow us to declare `Map` as
injective? Injectivity says you can deduce LHS from RHS but I think that
it would not be a good idea to try to solve `Map f [a, b] ~ [Int, Char]`.
And so the restriction on not having calls to type families on the RHS
would rightly declare `Map` as not injective. So if we had partially
applied type families and thus `f` was allowed to be either a type
constructor a type family we should declare `Map` as not injective. This
contrasts with earlier paragraph, where knowing that `f` must be a type
constructor allowed us to declare `Map` as injective.
>
> Does that make sense?
No. Under the singletons work, we gave a different kind to non-injective
functions, so Gabor's kind -- using `->`, not any other arrow -- requires
an injective argument.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:80>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
#6018: Injective type families
-------------------------------------+-------------------------------------
Reporter: lunaris | Owner: jstolarek
Type: feature | Status: new
request | Milestone: 7.10.1
Priority: normal | Version: 7.4.1
Component: Compiler | Keywords: TypeFamilies,
Resolution: | Injective
Operating System: | Architecture: Unknown/Multiple
Unknown/Multiple | Difficulty: Unknown
Type of failure: | Blocked By:
None/Unknown | Related Tickets: #4259
Test Case: |
Blocking: |
Differential Revisions: Phab:D202 |
-------------------------------------+-------------------------------------
Comment (by goldfire):
Replying to [comment:73 jstolarek]:
> 2. That condition must contain only the result type variable on the LHS
of `->` and all other type variables on the RHS of `->`. In other words if
I declare `type family P a b = r` then I'm only allowed to write `r -> a
b` or `r -> b a` injectivity condition. Questions here: a) can I add a
restriction that type variables on the RHS must be given in exactly the
same order as they were given in the head declaration? This would make the
implementation simpler; b) where should this check be done? In the
renamer?
I'm ambivalent on this design decision (that the variables have to be in
the same order in the annotation). I suppose it simplifies the
implementation. Yes, the renamer seems like a fine-enough place to do the
check.
>
> 3. Once we check 2) we must verify that the type family is indeed
injective. Not sure where this should happen? My guess is that during
typechecking of a type family equations. Algorithm is outlined
[wiki:InjectiveTypeFamilies#Implementationoutline here].
Please see updates to the wiki page, labeled '''RAE''' ... '''End RAE'''.
>
> Does the implementation plan outlined so far look sensible? Are there
any misconceptions?
>
> 4. Once we pass these checks injectivity becomes a binary property, so
we can discard injectivity conditions written by the user and replace it
with a `Bool`. Richard, when we first spoke about injective type families
you suggested that all the magic will go into `isDecomposableTyCon` in
`types/TyCon.lhs`. I've added a `Bool` field to `SynTyCon` data
constructor of `TyCon` data type and made `isDecomposableTyCon` use that
field to tell whether a type family is injective or not. (Checks described
in 2 and 3 are not implemented. When a user writes injectivity declaration
for a type family I just assume it is correct.) Sadly, this does not work.
Here's an example test case:
>
> {{{#!hs
> type family F a = r | r -> a where
> F Int = Bool
> F Bool = Int
> F a = a
>
> foo :: F a -> F a
> foo = id
> }}}
>
> This fails with:
>
> {{{
> Couldn't match type ‘F a0’ with ‘F a’
> NB: ‘F’ is a type function, and may not be injective
> The type variable ‘a0’ is ambiguous
> Expected type: F a -> F a
> Actual type: F a0 -> F a0
> In the ambiguity check for: forall a. F a -> F a
> To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
> In the type signature for ‘foo’: foo :: F a -> F a
> }}}
>
> I added traces to verify that `isDecomposableTyCon` is called for `F`
type family and it correctly returns `True`.
>
> Out of curiosity I turned on `AllowAmbiguousTypes` and added a
definition like this:
>
> {{{
> bar :: Int -> Int
> bar = foo
> }}}
>
> That failed with:
>
> {{{
> Couldn't match type ‘F a0’ with ‘Int’
> The type variable ‘a0’ is ambiguous
> Expected type: Int -> Int
> Actual type: F a0 -> F a0
> In the expression: foo
> In an equation for ‘bar’: bar = foo
> }}}
>
> I imagine that getting this one to work definitely requires more changes
than just `isDecomposableTyCon`.
Yes, Simon's comment above is correct -- I was just wrong about the
`isDecomposableTyCon` thing. Actually, injective type families still need
to say "no" to `isDecomposableTyCon`, because of the '''left''' and
'''right''' coercion formers, which assume generativity.
> Then again GHC can already deal with some cases of injectivity:
>
> {{{#!hs
> type family F a = r | r -> a where
> F Int = Int
> F Bool = Bool
> F a = a
>
> foo :: F a -> F a
> foo = id
>
> bar :: Int -> Int
> bar = foo
> }}}
>
> That works perfectly fine in GHC 7.8.
What works perfectly fine? Not the code you wrote above, because it
contains a not-currently-parsed injectivity annotation. I tried it without
the injectivity annotation, and it does indeed work. But not because of
injectivity, at all: it's because GHC is clever enough to figure out that
`F` is just an identity function, and so the `F a`s in `foo`'s type become
`a`. If you swap the `Int` and `Bool` RHSs in the definition (which
preserves injectivity), the code fails to compile.
>
> I tried to analyse what's going on with `-ddump-tc-trace` but the dumps
are 600-1000 lines long. Of course the source code itself is even longer,
so I'd appreciate any directions where should I start looking.
Fair warning: 1000 lines of `-ddump-tc-trace` isn't long at all! :)
>
> One final question. Assuming that `SynTyCon` really should have a new
field, I believe this field should be stored in interface files. After all
we want injectivity information to propagate from one module to another.
Now I wonder how this interacts with open type families. I understand that
these are typechecked progressively as we find more equations. I haven't
looked at the implementation but my intuition from reading GHC papers is
that in a given module we import open type family equations from other
modules, collect equations from current module and proceed with type
checking of an open type family. Is that intuition correct? If so then I
believe that checking of injectivity (point 3 of my outline) should be
done during this stage (I believe it would be best to combine it with
checking equation overlapping).
Agreed.
--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:79>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
