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 t

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 def

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 A

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 easy

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 > > On Thu, May 24, 201

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 there such a type > somewhere e

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 keep

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 sooner.) A great way to do this

Re: Superclass Equality constraints cp FunDeps

llbery wrote: > > On Sun, Apr 30, 2017 at 3:31 PM, Richard Eisenberg <mailto:r...@cs.brynmawr.edu>> wrote: > > On Apr 30, 2017, at 6:37 AM, Anthony Clayden > <mailto:anthony_clay...@clear.net.nz>> wrote: > > Is that behaviour officially documented somewhere? &

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. Otherwise, I agree with your notes.

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. on Equality Constraints] > >>

Re: Narrower (per-method) GND

gt; 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 instanc

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 wou

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 standardize some subset

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 to change. > And > th

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 the stated goals of

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. Additionally, GitHub is pro

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 development, but not

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 `Un n' >In the type synonym in

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

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,

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 wrote: >> From: AntC >> Date: 2015-06-04 22:39:25 GMT >> >>

Re: Closed Type Families: separate instance groups?

On Jun 3, 2015, at 7:09 PM, AntC 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 the earlier version. You can

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 Apr

Re: Increased memory usage with GHC 7.10.1

Post a bug report! :) On Apr 2, 2015, at 8:19 AM, Jan Stolarek 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 > build the module was

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 http://www.haskell.org/mailman

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, p

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

forall proxy (n :: Nat). (n `LeNat` Bound) ~ True => proxy n -> String > f _ = "It worked!" I'm happy to answer questions, but it's hard to know how much detail to use in a description of the code. I hope this helps, Richard On Dec 4, 2014, at 5:50 PM, Alexander

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

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 wrote: > I recently got a confusing error msg, and reduced it t

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

and having clever constructor only, >>> then the only place >>> where you need to check will be that constructor. >>> >>> Also it's possible to write in slightly clearer, but again it's >>> possible to make a mistake here >>> and it will

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 w

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 wrote: > To be clear: GHC can still typecheck, compile, and efficiently execute > Haskell 2010 code. It is merely the distribution of compatible > packages that has put us in someth

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: 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 w

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 s

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 u

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 wrote: > Proposal

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, na

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 t

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. Richard

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

hat > is considered “Safe”, 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 Ei

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 wou

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 wrote: > Hello, > > this is clearly a bug in GHC: where `B` and `C` are imported, there should > have been an error, sayin

Re: Overlapping and incoherent instances

I think one nice thing about this proposal is that it doesn't seem (to me) to require CPP around the pragma: unrecognized pragmas are warned about but are otherwise harmless. Are folks very keen to have *warning-free* compilation on several GHC versions? Personally, I would aim for warning-free

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,

Re: Closed type families, apartness, and occurs check

heck would seem to > prevent IsEq (G a) [G a] from ever evaulating to true. > > Brandon > > > On Wednesday, July 2, 2014 7:11 AM, Richard Eisenberg > wrote: > > > Hi Brandon, > > Yes, this is a dark corner of GHC wherein a proper dragon lurks. > > In

Re: Closed type families, apartness, and occurs check

Hi Brandon, Yes, this is a dark corner of GHC wherein a proper dragon lurks. In your second example, you're suggesting that, for all types `a`, `a` is never equal to `[a]`. The problem is: that's not true! Consider: > type family G x where > G x = [G x] This is a well-formed, although pathol

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, a

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

On May 31, 2014, at 1:12 AM, adam vogt 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 = False > type ins

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. Daniel

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

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?

, while I'm > learning more details of Core (and of HERMIT which I'm using to manipulate > Core). > > I'm now working on reification in the presence of casts. The rule I'm trying > to implement is > > > evalEP e |> co --> evalEP (e |> co'

Re: Help with coercion & roles?

en > produces > > > (LambdaCCC.Lambda.EP (Sym (Simple.NTCo:HasIf[0] _N)))_R > > And still I get "Role incompatibility: expected nominal, got representational > in `Sym (Simple.NTCo:HasIf[0] _N)`". > > I also tried wrapping `mkSubCo` around the entire co

Re: Help with coercion & roles?

I agree with Simon, but just `Sub` the `_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 and must produce rep

Re: positive type-level naturals

Nat > -- can't induct, hence crippled > type instance U n = Z > > > > > On Tue, Mar 18, 2014 at 9:33 AM, Richard Eisenberg wrote: > Yes, I suppose you would need UndecidableInstances. There's no way for GHC's > (already rather weak) termination checker to kn

Re: positive type-level naturals

that out > > I think i'm gonna go drop 7.6 support on some code i'm working on if this > works :) > > > > > > On Mon, Mar 17, 2014 at 2:05 PM, Richard Eisenberg wrote: > So much to respond to! > > First, a little relevant context: I

Re: type-level induction on Nat

On Mar 16, 2014, at 6:29 AM, Henning Thielemann wrote: > > Since the unary natural number kind so ubiquituous in examples, is there a > recommended module to import it from, which also contains the injectivity > magic of FromNat1? I cannot see it in: > No. After some debate (on the libraries

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: 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: Functional dependencies can "return" kinds, type families cannot

On Feb 13, 2014, at 4:28 AM, José Pedro Magalhães 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?... Yes,

Re: Enabling TypeHoles by default

Perhaps I'm being silly, but if the extended errors are enabled by default, and they seem to cause no problems, does the feature even need a name? The release notes could say something like "extended type information is produced for out-of-scope variables beginning with an underscore" or similar

Re: Decomposition of given equalities

ent kinds (how could you > ever have constructed `f a ~ g b` if they did?), but GHC isn't > equipped to reason about that (to store evidence for it and retrieve > it later)? > > On Thu, Dec 19, 2013 at 4:01 PM, Richard Eisenberg wrote: >> Let me revise slightly. GHC would

Re: Decomposition of given equalities

ot;nth" coercion, which allows decomposition of things like (T 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. > &g

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 coe

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 > bad

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 superc

Re: default roles

On Oct 9, 2013, at 6:24 PM, Joachim Breitner 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 consequence of this des

Re: default roles

On Oct 9, 2013, at 3:41 PM, Joachim Breitner 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. You're absolutely rig

Re: default roles

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 wrote: > I do

Re: default roles

gt; In other words, we are pretending that we are implementing all methods by > using `coerce`. > > As far as I can see this safe, and matches what I'd expect as a programmer. > It also solves the problem with the `Set` example: because `Set` has a > nominal parameter, we ca

Re: default roles

gure out how to do it. > > > On Tue, Oct 8, 2013 at 12:01 PM, José Pedro Magalhães > wrote: > Hi, > > On Tue, Oct 8, 2013 at 3:21 AM, Richard Eisenberg wrote: > We considered this for a while, but it led to a strange design -- to do it > right, you would have to i

Re: default roles

e to (C Age) by hand? To me, it looks like we 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 wrote: > Hi, > > On Tue, Oct 8, 2013 at 3:21 AM, Ric

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 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

Re: default roles

icitly state that t's type > parameter should always 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 написал(а): > >> As you may hav

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 retrof

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 instan

Re: 7.8 Release Update

On Sep 8, 2013, at 7:27 PM, Austin Seipp 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 error, which

Re: New restrictions to open type families

n) > > Thank you very much for your detailed explanation! > > > On Fri, Aug 23, 2013 at 1:24 PM, Richard Eisenberg 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&#

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) rests

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 rol

Re: Repeated variables in type family instances

type instance Default (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 : >> >> The nub o

RE: Repeated variables in type family instances

sed 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 Eisenberg : > > (Sorry for the re-send - got the wrong subject line last time.) >

RE: Repeated variables in type family instances - UndecidableInstances

ow-haskell-users@haskell.org > Subject: Re: Repeated variables in type family instances - > UndecidableInstances > > > Richard Eisenberg cis.upenn.edu> writes: > > > > ... The plan of action is to use the check labeled (B) > > on the wiki page. This check do

Re: Repeated variables in type family instances

e it made for a more consistent feature, in our 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 cis.upenn.edu> writes: >> >> And, in response to

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 Jeroen

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 ex

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 instanc

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

Re: Allowing (Char ~ Bool => Void)?

le and what isn't. > I can't say I'm enthusiastic here. To be fair, neither am I. This was just one 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 > th

Re: Allowing (Char ~ Bool => Void)?

ode" be a warning > rather than an error? > > Would you care to make a ticket with a clear specification? Thanks! > > Simon > > | -Original Message- > | From: glasgow-haskell-users-boun...@haskell.org [mailto:glasgow-haskell- > | users-boun...@haskel

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 t

  1   2   >