We do need a separate category, though: otherwise, we could cast by `f x`, where `f` is a non-terminating functions. We erase casts, so the function would never get called. Maybe if we required that casts are always by variables (essentially, A-normalize casts) we could avoid this? But then would we require A-normalization to build coercions from pieces (as opposed to calling functions)? It's unclear.
I think the first versions of this idea didn't require the separate syntactic category, but all work for the past decade has. I think there are other ways, but the way GHC handles this now is somewhat poor, because of #17291. Richard > On Feb 5, 2021, at 7:56 PM, Igor Popov <mn...@typeable.io> wrote: > >> GHC cheats in this area. The problem is that (a ~# b) is a type, because >> that is terribly, terribly convenient. But it really shouldn't be. >> >> The problem is that coercion variables are different from regular variables. >> So, if we say (v :: a ~# b), we must always be careful: is v a coercion >> variable or not? If it isn't, then v is useless. You cannot, for instance, >> use v in a cast. > > I don't really see a problem here. The fact that only a "coercion > variable" can be used in a cast should be enforced by the typing rule > for cast. That doesn't require having a distinct "syntactic category" > of coercion variables, unless I'm missing something. > > -- mniip _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
