Re: Getting valid substitutions to work for subsumption

2017-05-18 Thread Richard Eisenberg
> On May 18, 2017, at 5:27 PM, Simon Peyton Jones wrote: > > I don't agree. If you call (tcSubsumes hole_ty ty) with closed types > hole_ty, ty, it should return True if I agree here. But it looks like Matthías's function gets the expected type as pushed down by

RE: Getting valid substitutions to work for subsumption

2017-05-18 Thread Simon Peyton Jones via ghc-devs
vs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Richard | Eisenberg | Sent: 18 May 2017 14:21 | To: Matthías Páll Gissurarson <m...@mpg.is> | Cc: ghc-devs@haskell.org | Subject: Re: Getting valid substitutions to work for subsumption | | Hi Matthías, | | This is going to be challenging

Re: Getting valid substitutions to work for subsumption

2017-05-18 Thread Richard Eisenberg
Hi Matthías, This is going to be challenging to fix, I'm afraid. When GHC sees a definition with a polymorphic type signature, it *skolemizes* the signature before ever looking at the definition. In this context, skolemizing means that GHC will fix the type variable a (in your trace, it