Re: Can I create a representation polymorphic datatype?

Hi Clinton, Sadly, GHC does not support what you want. I don't really have much more to add to your post, which accurately describes the problem and correctly describes why we can't have one compiled function that works at multiple representations. The canonical ticket for this kind of feature

Re: Typing of Pattern Synonyms: Required vs Provided constraints

> On Jan 5, 2022, at 9:19 PM, Anthony Clayden > wrote: > > So Pattern syns seem to be giving exactly the 'stupid theta' behaviour. In your example, yes: the Required context is "stupid" in the way that "stupid theta" is. The reason to have a Required context is if your pattern synonym does

Re: Pattern synonym constraints :: Ord a => () => ...

; > On Tue, Oct 5, 2021, 12:33 PM Richard Eisenberg <mailto:li...@richarde.dev>> wrote: > > >> On Oct 3, 2021, at 5:38 AM, Anthony Clayden > <mailto:anthony.d.clay...@gmail.com>> wrote: >> >> >pattern SmartConstr :: Ord a =>

Re: Pattern synonym constraints :: Ord a => () => ...

> On Oct 3, 2021, at 5:38 AM, Anthony Clayden > wrote: > > >pattern SmartConstr :: Ord a => () => ... > > Seems to mean: > > * Required constraint is Ord a -- fine, for building Yes. > * Provided constraint is Ord a -- why? for matching/consuming No. Your signature specified that

Re: How to user-define a type equality constraint?

> On Apr 6, 2021, at 7:44 AM, Anthony Clayden > wrote: > > > But why does this matter? > > Because I want the semantics of that equality constraint, without switching > on any of these, which I don't otherwise use: > > GADTs > TypeFamilies > TypeOperators > > And if that means I can't use

Re: How to user-define a type equality constraint?

> On Apr 1, 2021, at 8:12 PM, Anthony Clayden > wrote: > > Can I user-define a conventional type-class that behaves more like `(~)`? I don't think so. But why does this matter? I can't define `Char` in user code, but it's exported from the Prelude and requires no extensions. While I can

Re: Pattern synonym 'Required' constraints === Datatype Contexts(?)

No hidden Bool here -- this is just a consequence of the way that view patterns work, where you have to match against the result of the function, in this case, (>0). See https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/view_patterns.html Richard > On Mar 12, 2021, at 6:37

Re: Pattern synonym 'Required' constraints === Datatype Contexts(?)

You're right that these features sit in a similar space. The difference is that, with a pattern synonym, the required context might be useful. This is because pattern synonyms can perform computation (via view patterns), and this computation might plausibly require some class constraint. An

Re: [ANNOUNCE] GHC 8.6.1-beta1 available

> On Aug 11, 2018, at 11:27 AM, Vassil Ognyanov Keremidchiev > wrote: > > What are the new features there toward Dependent Typed Haskell? Ben's link to https://downloads.haskell.org/~ghc/8.6.1-beta1/docs/html/users_guide/8.6.1-notes.html

Re: Natural number comparisons with evidence

Just to add my 2 cents: I've played in this playground and used the same structures as David. I second his suggestions. Richard > On May 24, 2018, at 3:54 PM, Conal Elliott wrote: > > Great! Thanks for the suggestion to use type equality and coerced `Refl`. - > Conal > >

Re: Heterogeneous equality

> On Jul 5, 2017, at 5:23 PM, Wolfgang Jeltsch wrote: > > Hi! > > The base package contains the module Data.Type.Equality, which contains > the type (:~:) for homogeneous equality. I was a bit surprised that > there is no type for heterogeneous equality there. Is

Re: Trouble with injective type families

I'd like to add that the reason we never extended System FC with support for injectivity is that the proof of soundness of doing so has remained elusive. A similar unsoundness in type improvement may cause unpredictable behavior in type inference, but it can't ever launch the rockets. So we

Re: Superclass Equality constraints cp FunDeps

> On May 7, 2017, at 8:42 PM, Anthony Clayden > wrote: > > Is that worth adding to the docos? The best way to evaluate this is to submit a concrete patch -- better if it’s a patch directly to the manual than just a note on Trac. (Better ==> it will be adopted

Re: Superclass Equality constraints cp FunDeps

allber...@gmail.com> wrote: > > On Sun, Apr 30, 2017 at 3:31 PM, Richard Eisenberg <r...@cs.brynmawr.edu > <mailto:r...@cs.brynmawr.edu>> wrote: > > On Apr 30, 2017, at 6:37 AM, Anthony Clayden <anthony_clay...@clear.net.nz > > <mailto:anthony_clay...@clear.

Re: Superclass Equality constraints cp FunDeps

> On Apr 30, 2017, at 6:37 AM, Anthony Clayden > wrote: > > Is that behaviour officially documented somewhere? Not that I can find. Documentation on functional dependencies is somewhat lacking. This may be because fundeps has received little love of late.

Re: Superclass Equality constraints cp FunDeps

I'm not quite sure what a restriction on (~) might be, but (~) is effectively declared as > class a ~ b | a -> b, b -> a So I agree with your observations. Richard > On Apr 27, 2017, at 8:14 PM, Anthony Clayden > wrote: > > The docos say [User Guide 10.14.1.

Re: Narrower (per-method) GND

all a. > ReaderT Int m (ReaderT Int m a) -> ReaderT Int m a’ > to type ‘forall a. N m (N m a) -> N m a’ > NB: We cannot know what roles the parameters to ‘m’ have; > we must assume that the role is nominal > • When deriving the insta

Re: Narrower (per-method) GND

I agree with David that using explicit `coerce`s can be quite verbose and may need ScopedTypeVariables and InstanceSigs. But visible type application should always work, because class methods always have a fixed type argument order. Regardless, requiring users to do all this for GND on Monad

Re: Proposal process status

> On Jul 21, 2016, at 2:25 PM, Yuras Shumovich wrote: > > It is hopeless. Haskell2020 will not include TemplateHaskell, GADTs, > etc. Why do you say this? I don't think this is a forgone conclusion. I'd love to see these standardized. My own 2¢ on these are that we can

Re: Proposal process status

> On Jul 21, 2016, at 11:29 AM, Yuras Shumovich wrote: > > Unfortunately Haskell *is* implementation-defined language. You can't > compile any nontrivial package from Hackage using Haskell2010 GHC. Sadly, I agree with this statement. And I think this is what we're trying

Re: Proposal process status

> On Jul 21, 2016, at 10:32 AM, Gershom B wrote: > > On July 21, 2016 at 8:51:15 AM, Yuras Shumovich (shumovi...@gmail.com) wrote: >> >> It makes sense to have >> two committees only if we have multiple language implementations, but >> it is not the case. > I disagree. By

Re: Proposal process status

> On Jul 20, 2016, at 12:47 PM, Alexander Berntsen wrote: > > On 20/07/16 11:36, Ben Gamari wrote: >> * What would you like to see changed in the proposed process, if >> anything? > No GitHub. In order to fully utilise GitHub, one needs to run > proprietary programs.

Re: Feedback on -Wredundant-constraints

I've been bitten by this too and had to disable the warning. Let me propose an alternative; * -Wredundant-constraints becomes only your Warning 1. That is, it reports when a user writes a constraint that is fully equivalent to some other, strictly smaller constraint, like suggesting simplifying

Re: Reconsidering -Wall and -Wcompat

On Feb 14, 2016, at 1:51 PM, Sven Panne wrote: > > IMHO, the distinction between "during development" and "outside of it" is > purely hypothetical. I find this comment quite interesting, as I see quite a large difference between these.* For example, I use -Werror during

Re: suppress warning "Defined but not used: type variable ‘x’" in GHC-8.0

On Jan 9, 2016, at 6:44 PM, Henning Thielemann wrote: > > instance (Natural n) => Num.Integer (Un n) where >type Repr (Un _n) = Unary > > > GHC-7.6.3 and GHC-7.4.2 complain: >Type indexes must match class instance head >Found `Un _n' but expected

Re: Closed Type Families: type checking dumbness? [was: separate instance groups]

This is all expected behavior. GHC's lazy overlap checking for class instances simply cannot apply to type families -- it would be unsound. I'm afraid I don't see what can be improved here. Richard On Jun 6, 2015, at 2:04 AM, AntC anthony_clay...@clear.net.nz wrote: From: AntC Date:

Re: Closed Type Families: type checking dumbness? [was: separate instance groups]

to define classes by consecutive cases to match the family definitions. I don't know what a good syntax for that would be, since 'where' syntax is taken for those. But it seems like it would correspond fill the hole here. On Sun, Jun 7, 2015 at 7:27 AM, Richard Eisenberg e...@cis.upenn.edu wrote

Re: Closed Type Families: separate instance groups?

On Jun 3, 2015, at 7:09 PM, AntC anthony_clay...@clear.net.nz wrote: Is this separate instance group idea still a gleam in someone's eye? If not, is there some deep theoretical reason against? Not to my knowledge (to both questions). But I don't believe we've lost any expressiveness over

Re: Increased memory usage with GHC 7.10.1

I've pasted Michal's numbers in #9630, which seems like a good place to track this. Michal, would you mind fleshing out a bit precisely what you did to get those numbers? That would be helpful (though you've already been very helpful indeed in getting the data together)! Thanks, Richard On

Re: Increased memory usage with GHC 7.10.1

Post a bug report! :) On Apr 2, 2015, at 8:19 AM, Jan Stolarek jan.stola...@p.lodz.pl wrote: An update frrom my second machine, this time with 4GB of RAM. Compiling Agda ran out of memory (again Agda.TypeChecking.Serialise module) and I had to kill the build. But once I restarted the

Re: ghc-7.10.0 type inference regression when faking injective type families

After quite a bit of thought, I agree that this is a regression and that the original program should be accepted. Make a bug report! Thanks, Richard ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org

Re: Avoid blank line separating code and comments in Bird style?

I think the underlying problem here is that there is a difference between literate comments and normal comments. In a bird-style literate Haskell file, this is what I'll call a literate comment: ~~~ A line with no marker at the beginning ~~~ A normal comment is in a line of Haskell code, put

Re: Proving properties of type-level natural numbers obtained from user input

: Hi, Richard Can you give some ideas or where to read how to properly use signletons and unary naturals in order to be able to express such constraints? Thanks -- Alexander On 30 November 2014 at 23:26, Richard Eisenberg e...@cis.upenn.edu wrote: Hi Alexander, Nice idea to test

Re: confusing type error

The reason I said That's a bug! so confidently is because of the expected n but got n part. Even if everything else is OK, we need to fix that one bit. And I tend to agree about using heuristics to report better error messages in the presence of instantiating a type variable with (-). I've been

Re: confusing type error

This seems straightforwardly to be a bug, to me. HEAD gives the same behavior you report below. Please post on the bug tracker at https://ghc.haskell.org/trac/ghc/newticket Thanks! Richard On Dec 4, 2014, at 1:50 PM, Evan Laforge qdun...@gmail.com wrote: I recently got a confusing error msg,

Re: Proving properties of type-level natural numbers obtained from user input

= natVal k = Just (Proof $ Tagged (Proxy :: Proxy n)) | otherwise = Nothing Of cause solution using singletons could solve this problem much better. -- Alexander On 25 November 2014 at 21:34, Richard Eisenberg e...@cis.upenn.edu wrote: Hi Bas, I believe to do this right, you would

Re: Proving properties of type-level natural numbers obtained from user input

Hi Bas, I believe to do this right, you would need singleton types. Then, when you discover that the number is bounded by 255, you would also discover that the type is bounded by 255, and you'd be home free. Unfortunately, I there isn't currently a way to do comparison on GHC.TypeLits Nats

Re: The future of the Haskell98 and Haskell2010 packages

I support this direction. But I disagree with one statement you've made: On Nov 18, 2014, at 11:07 AM, Austin Seipp aus...@well-typed.com wrote: To be clear: GHC can still typecheck, compile, and efficiently execute Haskell 2010 code. It is merely the distribution of compatible packages that

Re: Irreducible predicates error in Template Haskell

This fix will not get merged into the 7.8.x development stream, but it is already available in HEAD and will be available in GHC 7.10.x. We try not to make breaking changes (and this is a breaking change) in the middle of a major version. Richard On Oct 29, 2014, at 11:27 AM, Sreenidhi Nair

Re: Recursion on TypeNats

I don't think we'll need notation to differentiate: just use overloaded literals, like we do in terms. Something that would operate vaguely like this: type family 3 :: k where 3 :: Nat = ... -- 3 as a Nat 3 :: Integer = ... -- 3 as an Integer I'm not at all suggesting it be implemented

Re: Recursion on TypeNats

No, there's not another way to do this with built-in Nats, and there probably won't ever be. There are two advantages to the built-in Nats over hand-rolled ones: 1) Better syntax / error messages. 2) Built-in Nats are much more efficient than hand-rolled ones, because the hand-rolled ones are

Re: Recursion on TypeNats

Your argument here is compelling. I have wanted type-level integers from the beginning and saw Nats as just a step toward integers. But, of course, this is silly -- you're right that Nats deserve their own place. Perhaps make a feature request for this. It may be related to type-level pattern

Re: Hiding import behaviour

Thanks for writing this up so clearly. I'm +1 on the proposal as written. I think the (smallish) drawbacks are mitigated by the fact that the whole feature is opt-in. Implementation should be relatively straightforward. Thanks, Richard On Oct 23, 2014, at 2:22 PM, htebalaka goodi...@gmail.com

Re: Hiding import behaviour

I'm having a hard time keeping track of what's going on in this discussion. But, I'm generally in favor of making *some* change along the lines discussed here, and also in #9702 (https://ghc.haskell.org/trac/ghc/ticket/9702). Could the proposers of various features perhaps create a wiki page,

GADTs in implementation of Template Haskell

I'm doing a bunch of bug-fixes / improvements to Template Haskell. Two of these are to fix GHC bugs #8100 (add standalone-deriving support) and #9064 (add `default` method type signature support), both of which introduce new constructors for `Dec`. This got me thinking about `Dec` and the fact

Re: Permitting trailing commas for record syntax ADT declarations

To be fair, I'm not sure I like the make-commas-optional approach either. But, the solution occurred to me as possible, so I thought it was worth considering as we're exploring the design space. And, yes, I was suggesting only to make them optional, not to require everyone remove them.

Re: Are safe coercions safe in the sense of Safe Haskell?

”, although the discussions on Trac concluded that this should not be the case. You can just import coerce via GHC.Prim, which is “Safe-Inferred”. All the best, Wolfgang Am Freitag, den 15.08.2014, 19:40 -0400 schrieb Richard Eisenberg: See https://ghc.haskell.org/trac/ghc/ticket/8745

Re: Are safe coercions safe in the sense of Safe Haskell?

See https://ghc.haskell.org/trac/ghc/ticket/8745 and https://ghc.haskell.org/trac/ghc/ticket/8827 which discuss this problem at length. The short answer: It's conceivable that a role-unaware library author would have abstraction expectations that are defeated through the use of `coerce`. I

Re: Overlapping and incoherent instances

This has been reported: https://ghc.haskell.org/trac/ghc/ticket/8338 But it's really not clear what the solution is! Richard On Aug 11, 2014, at 9:27 PM, Iavor Diatchki iavor.diatc...@gmail.com wrote: Hello, this is clearly a bug in GHC: where `B` and `C` are imported, there should have

Re: Type family stopped compiling on upgrade from GHC 7.6.3 to 7.8.3

This seems to be a bug in GHC. I can write the Show instance manually: instance (Show c, Show d) = Show (CmpInterval (V c) (V d)) where show (c `Interval` d) = show c ++ `Interval` ++ show d Perhaps you should file a bug report -- your code looks sensible to me. Richard On Jul 23, 2014, at

Re: Closed type families, apartness, and occurs check

to prevent IsEq (G a) [G a] from ever evaulating to true. Brandon On Wednesday, July 2, 2014 7:11 AM, Richard Eisenberg e...@cis.upenn.edu wrote: Hi Brandon, Yes, this is a dark corner of GHC wherein a proper dragon lurks. In your second example, you're suggesting

Re: Associated type instances

I'm sure I've used the feature that you're proposing to remove, but I'll adapt. To be clear, the change means no loss of expressiveness, just that I'll sometimes have to use a helper type family (closed or open), right? If I'm right there, then no complaints from me. Richard On Jun 24, 2014,

Re: Data.Type.Equality.== works better when used at kind * - * - Bool

On May 31, 2014, at 1:12 AM, adam vogt vogt.a...@gmail.com wrote: are there instances of (==) that behave differently from the poly-kinded version? Yes. To be concrete, here would be the polykinded instance: type family EqPoly (a :: k) (b :: k) where EqPoly a a = True EqPoly a b =

Re: vector and GeneralizedNewtypeDeriving

Is this an instance of https://ghc.haskell.org/trac/ghc/ticket/8177 ? I think so. The problem boils down to the fact that Vector and MVector are data families and are thus (currently) exempted from the roles mechanism. (Or, more properly, may *only* have nominal roles.) There is no technical

Re: question about GADT's and error messages

My understanding of OutsideIn leads me to believe that GHC 7.8 has the behavior closer to that spec. See Section 5.2 of that paper (http://research.microsoft.com/en-us/um/people/simonpj/Papers/constraints/jfp-outsidein.pdf), which is a relatively accessible explanation of this phenomenon.

Re: Removing -fext-core

+1 from me I’ve been meaning to say essentially the same thing as you just did. We all seem to concentrate on *adding* things to GHC; it’s a bit refreshing to consider *removing* something. Echoing Austin somewhat: - Anyone using external core is either working with an old GHC or is kludging

Re: Type/type class information in GHC plugin

Hello Shen, I’m not sure if I’m answering exactly what you’re asking, but perhaps this can move you in the right direction: - To apply an expression to some types, you can use mkTyApps, in the CoreSyn module. The type of that function (Expr b - [Type] - Expr b) should be self-explanatory. -

Re: Concrete syntax for open type kind?

What version of the GHC code are you looking at? The parser is currently stored in compiler/parser/Parser.y.pp (note the pp) and doesn’t have these lines. As far as I know, there is no way to refer to OpenKind from source. You’re absolutely right about the type of `undefined`. `undefined` (and

Re: Help with coercion roles?

I agree with Simon, but just `Sub` the `LambdaCCC.Lambda.EP_N`, not the whole coercion. There are actually two problems here. The one Simon identified, and also the fact that Simple.NTCo:HasIf[0] produces a representational coercion. How do I know? Because of the `NT` -- it's a newtype axiom

Re: Help with coercion roles?

the entire coercion (applying `mkSubCo . mkAppCo (Refl Nominal ep)`), and I see the same result: (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] GHC.Types.Bool_N)))_R -- Conal On Mon, Apr 14, 2014 at 4:39 AM, Richard Eisenberg e...@cis.upenn.edu wrote: I agree with Simon, but just `Sub

Re: Help with coercion roles?

a ~ EP b`. I'm trying to build `co'` from `co`, which led to these questions. So what do you think? Is there a sound coercion I can build for `co'`? -- Conal On Mon, Apr 14, 2014 at 11:54 AM, Richard Eisenberg e...@cis.upenn.edu wrote: Hi Conal, In your case, the `_N` on the argument

Re: positive type-level naturals

, 2014 at 9:33 AM, Richard Eisenberg e...@cis.upenn.edu wrote: Yes, I suppose you would need UndecidableInstances. There's no way for GHC's (already rather weak) termination checker to know that by saying (n-1) a bunch, you're bound to reach 0. I'm glad it's working for you. When I discovered

Re: positive type-level naturals

So much to respond to! First, a little relevant context: Iavor Diatchki is the primary implementor of the type-lits stuff; I am not. But, he and I are playing in the same playground, so to speak, so we confer a fair amount and I may have some helpful perspective on all of this. Henning asks:

Re: converting data-level natural numbers to type-level

On Mar 15, 2014, at 4:48 PM, Henning Thielemann wrote: What is the meaning of KnownNat? It is a Nat whose value is known at runtime. I'll confess to suggesting the name… I think I was hoping there would be more debate and a better idea at the time, but it just stuck. I see that there is no

Re: Functional dependencies can return kinds, type families cannot

On Feb 13, 2014, at 4:28 AM, José Pedro Magalhães j...@cs.uu.nl wrote: The most interesting part here is the functional dependency fs - k, where k is a kind variable! If this is not a bug (and it does seem to work as I expect it to), then could we have type families return kinds too?...

Re: Decomposition of given equalities

a ~ T b).) Good -- I feel much better about this answer, where there's no guess for the value of f3! Richard On Dec 18, 2013, at 11:30 PM, Richard Eisenberg wrote: I'd say GHC has it right in this case. (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the kinds match up. If, say

Re: Decomposition of given equalities

I'd say GHC has it right in this case. (f a ~ g b) exactly implies (f ~ g) and (a ~ b) if and only if the kinds match up. If, say, (f :: k1 - *), (g :: k2 - *), (a :: k1), and (b :: k2), then (f ~ g) and (a ~ b) are ill-kinded. In Gabor's initial problem, we have (with all type, kind, and

Re: default roles

On Oct 10, 2013, at 1:14 PM, David Menendez wrote: Sure, but if op uses show internally, we get Int's show, not Age's, right? That seems correct, in that it's doing what GND is supposed to do, but I'll bet it will surprise people. Yes, you're right. If a method in a subclass uses a

Re: default roles

Please see below. On Oct 10, 2013, at 10:09 PM, Edward Kmett wrote: Wait, that sounds like it induces bad semantics. Can't we use that as yet another way to attack the sanctity of Set? class Ord a = Foo a where badInsert :: a - Set a - Set a instance Foo Int where badInsert =

Re: default roles

of `MyAge` for `HasSet`. An added benefit of this approach is that when newtype deriving fails, we can give a nicer error saying exactly which method causes the problem. -Iavor On Mon, Oct 7, 2013 at 6:26 AM, Richard Eisenberg e...@cis.upenn.edu wrote: As you may have heard

Re: default roles

a data type to coerce a dictionary. It seems likely that I could do it with just a well crafted function argument and ScopedTypeVariables, but my version of HEAD is a bit too mangled at the moment to give it a try. -Edward On Wed, Oct 9, 2013 at 2:09 PM, Richard Eisenberg e

Re: default roles

On Oct 9, 2013, at 3:41 PM, Joachim Breitner m...@joachim-breitner.de wrote: what do you need the extra bit for? During GHD, can’t you just create the new dictionary (using method = coerce original_method) and then see if it typechecks, i.e. if the method types can be coerced. Efficiency.

Re: default roles

On Oct 9, 2013, at 6:24 PM, Joachim Breitner m...@joachim-breitner.de wrote: So the conclusion is indeed: Let type class constraints have a nominal role, and all is fine. But, then it would seem that any class with a superclass wouldn't be compatible with GND. Do you see that detail as a

Re: default roles

need MkT and S2, but not S1. Yet, this is not obvious and seems to be quite confusing. I hope this helps understanding the issue! Richard On Oct 8, 2013, at 4:01 AM, José Pedro Magalhães drei...@gmail.com wrote: Hi, On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg e...@cis.upenn.edu wrote: We

Re: default roles

:21 AM, Richard Eisenberg e...@cis.upenn.edu wrote: We considered this for a while, but it led to a strange design -- to do it right, you would have to import all constructors for all datatypes *recursively* out to the leaves, starting at the datatypes mentioned in the class for which you

default roles

As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism to allow for safe 0-cost conversions between newtypes and their base types. GeneralizedNewtypeDeriving (GND) already did this for class instances, but in an unsafe way -- the feature has essentially been

Re: default roles

be representational, and b) at the same time make a representational. Seems like a probable scenario to me. Отправлено с iPad 07 окт. 2013 г., в 17:26, Richard Eisenberg e...@cis.upenn.edu написал(а): As you may have heard, /roles/ will be introduced with GHC 7.8. Roles are a mechanism

Re: default roles

lot of imports for symbols not actually used in the text of a program. Richard On Oct 7, 2013, at 4:33 PM, Ganesh Sittampalam gan...@earth.li wrote: Is it possible to tie the role to whether the data constructor is visible or not? On 07/10/2013 14:26, Richard Eisenberg wrote: As you may have

Re: Desugaring do-notation to Applicative

The soundness of this desugaring depends on the Applicatives and Monads following some of the laws. I think that's OK, personally, but this assumption should be made loudly somewhere, and the feature should be opt-in. As far as I know, GHC currently makes no assumptions about lawful class

Re: 7.8 Release Update

On Sep 8, 2013, at 7:27 PM, Austin Seipp ase...@pobox.com wrote: * Pedro and Richard - what's the story on propositional equality, etc? This is mentioned on the status page[1] but I'm not sure what else needs to be done. I know Pedro committed the work to make manual Typeable instances an

Re: New restrictions to open type families

very much for your detailed explanation! On Fri, Aug 23, 2013 at 1:24 PM, Richard Eisenberg e...@cis.upenn.edu wrote: This is a good question. Happily, there are at least two decent answers. 1) We're not sure that this problem cannot cause a segfault… it's just that we've been unable

Re: New restrictions to open type families

This is a good question. Happily, there are at least two decent answers. 1) We're not sure that this problem cannot cause a segfault… it's just that we've been unable to produce one when trying. Perhaps we haven't tried hard enough. 2) The type soundness of Haskell (as implemented in GHC)

Re: Marking type constructor arguments as nominal (e.g. Set)

The recommended way to do this (force a Nominal parameter) is {-# LANGUAGE RoleAnnotations #-} data Set a@N = Set a The @N annotation forces `a`'s role to be Nominal, as desired, but makes no other change to the type. Note that role annotations can only increase roles -- you can't use role

Re: Repeated variables in type family instances

(a :: * - * - * - *) = (,,) This isn't perhaps the most useful example, but it works. Richard On Jun 26, 2013, at 8:33 AM, Dominique Devriese wrote: Richard, Thanks for your answers. 2013/6/24 Richard Eisenberg e...@cis.upenn.edu: The nub of the difference is that type families can pattern-match on kinds

RE: Repeated variables in type family instances - UndecidableInstances

instances - UndecidableInstances Richard Eisenberg eir at cis.upenn.edu writes: ... The plan of action is to use the check labeled (B) on the wiki page. This check does *not* ban all nonlinear type families. Thanks Richard, great! Then the focus of attention moves to infinite types. I

RE: Repeated variables in type family instances

, and I'll add links from the wiki, etc. P.S.2: On an unrelated note: will you also do a completeness check on closed type family definitions? There is no plan for this, no. In the presence of non-linear equations, I'm not sure off the top of my head how I would do this. Richard 2013/5/29 Richard

Re: Repeated variables in type family instances

eyes. I'm really happy with where this ended up, so thanks for making the suggestion originally! Richard On Jun 22, 2013, at 10:28 AM, AntC wrote: Richard Eisenberg eir at cis.upenn.edu writes: And, in response to your closing paragraph, having type-level equality is the prime motivator

RE: Type families causing the compiler to hang on recompilation

If the problem is happening in HEAD, it's a legitimate bug. Please file a report and I'll take a look at it, as I'm in that area of the codebase right now. Thanks! Richard From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell-users-boun...@haskell.org] On Behalf Of

Re: Repeated variables in type family instances

On Jun 20, 2013, at 11:47 AM, AntC wrote: Hmm. Several things seem 'fishy' in your examples. I'll take the second one first: type family G type family G = [G] Your criticisms of this example (that it is nullary and unusable) are valid. But, it would be easy to change the example to

Branched type family instances

Hello all, It's come to my attention that there is a tiny lurking potential hole in GHC's type safety around type families in the presence of UndecidableInstances. Consider the following: type family F a b type instance F x x = Int type instance F [x] x = Bool type family G

Repeated variables in type family instances

(Sorry for the re-send - got the wrong subject line last time.) Hello all, It's come to my attention that there is a tiny lurking potential hole in GHC's type safety around type families in the presence of UndecidableInstances. Consider the following: type family F a b type instance

Re: Allowing (Char ~ Bool = Void)?

idea of a way to proceed. I'm happy to consider this idea abandoned. I WOULD like someone to help beef up the pattern-match overlap detector in the desugarer. That would be really useful. Simon | -Original Message- | From: Richard Eisenberg [mailto:e...@cis.upenn.edu

Re: Allowing (Char ~ Bool = Void)?

| -Original Message- | From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell- | users-boun...@haskell.org] On Behalf Of Richard Eisenberg | Sent: 24 March 2013 14:49 | To: Shachaf Ben-Kiki | Cc: glasgow-haskell-users | Subject: Re: Allowing (Char ~ Bool = Void

Re: Allowing (Char ~ Bool = Void)?

Though I've never run into the problem Shachaf mentions, this certainly seems useful. However, when testing Shachaf's code, I get the same error that I get when writing an impossible branch of a case statement. I imagine that the same code in GHC powers both scenarios, so any change would have

Re: Annotating an AST with type checking / source line number info

Disclaimer: I have worked on a few projects updating GHC itself; I have never used the GHC API. You've asked for two different things: location information and type information in an AST. The first is easy: it's already there, I believe. Many of the GHC types are prefixed with L. By

Re: runghc -fdefer-type-errors

When I ran this code (ghc 7.6.1), I did get the Hello, world! printout. That line was sandwiched between the compile-time warning from the type error and the run-time exception from the type error, but the output was there: 09:24:28 ~/temp runghc Scratch.hs Scratch.hs:5:12: Warning: No

Re: GHC 7.8 release?

Geoff's reasoning seems quite sound. +1 for February release. On Feb 7, 2013, at 3:50 AM, Geoffrey Mainland mainl...@apeiron.net wrote: In practice the versions of GHC that are widely used are those that are included in the platform. Maybe we should coordinate with their next release? They

Re: Advice on type families and non-injectivity?

Hi Conal, I agree that your initial example is a little puzzling, and I'm glad that the new ambiguity checker prevents both definitions, not just one. However, your initial question seems broader than just this example. I have run into this problem (wanting injective type functions) several

Re: Fundeps and type equality

online here http://www.haskell.org/ghc/dist/current/docs/html/users_guide/type-families.html#type-instance-declarations Simon From: Richard Eisenberg [mailto:e...@cis.upenn.edu] Sent: 11 January 2013 03:03 To: Carter Schonwald Cc: Martin Sulzmann; glasgow-haskell-b...@haskell.org

Re: Fundeps and type equality

(or at least implicit) about the overlapping type families from the docs is this: does it let me write recursive type level functions? (I really really really want that :) ) thanks -Carter On Thu, Jan 10, 2013 at 10:03 PM, Richard Eisenberg e...@cis.upenn.edu wrote: Yes, I finished

  1   2   >