On Fri, 7 Dec 2018 at 10:57 PM, Adam Gundry wrote: > > Regarding inference, the place that comes to mind is Vytiniotis et al. > OutsideIn(X): >
Thanks Adam for the references. Hmm That OutsideIn paper is formidable in so many senses ... I'm not sure I grok your response on my specific q; to adapt your example slightly, without a signature foo2 x@(_: _) = x GHC infers `foo2 :: [a] -> [a]`. That's not general enough. So I give a signature with bare `b` as the return type, using the (~) to improve it: foo2 :: [a] ~ b => [a] -> b ... and GHC infers `foo2 :: [a] -> [a]`. Oh. Is that what I should expect? I'm chiefly concerned about improving bare tyvars under a FunDep. So to take the time-worn example, I want instances morally equivalent to data TTrue = TTrue; data TFalse = TFalse class TEq a b r | a b -> r where tEq :: a -> b -> r instance TEq a a TTrue where tEq _ _ = TTrue instance TEq a b TFalse where tEq _ _ = TFalse The FunDeps via CHRs 2006 paper tells me that first instance is supposed to be as if instance (r ~ TTrue) => TEq a a r where ... but it isn't tEq 'a' 'a' :: TFalse -- returns TFalse, using the first pair of instances tEq 'a' 'a' :: TFalse -- rejected, using the (~) instance: 'Couldn't match type TFalse with TTrue ...' The 'happily' returning the 'wrong' answer in the first case has caused consternation amongst beginners, and a few Trac tickets. So what magic is happening with (~) that it can eagerly improve `foo2` but semi-lazily hold back for `tEq`? Of course I lied about the first-given two instances for TEq: instances are not consistent with Functional Dependency. So I need to resort to overlaps and a (~) and exploit GHC's bogus consistency check: instance {-# OVERLAPPABLE #-} (r ~ TFalse) => TEq a b r where ... > ... like automatically inferring where `typeCast` needs to be placed Yes the non-automatic `TypeCast` version instance (TypeCast TTrue r) => TEq a a r where tEq _ _ = TTrue -- rejected 'Couldn't match expected type 'r' with actual type 'TTrue' ...' tEq _ _ = typeCast TTrue -- accepted Even though `typeCast` is really `id` (after it's jumped through the devious indirection hoops I talked about). So what I'm trying to understand is not just "where" to place `typeCast` but also "when" in inference it unmasks the unification. AntC > About your specific question, if a wanted constraint `a ~ b` can be > solved by unifying `a` with `b`, then GHC is free to do so (in a sense, > either parameter of (~) can be improved from the other). The real > difference with `TypeCast` arises when local equality assumptions (given > constraints) are involved, because then there may be wanted constraints > that cannot be solved by unification but can be solved by exploiting the > local assumptions. > > For example, consider this function: > > foo :: forall a b . a ~ b => [a] -> [b] > foo x = x > > When checking the RHS of `foo`, a wanted constraint `[a] ~ [b]` arises > (because `x` has type `[a]` and is used in a place where `[b]` is > expected). Since `a` and `b` are universally quantified variables, this > cannot be solved by unification. However, the local assumption (given > constraint) `a ~ b` can be used to solve this wanted. > > This is rather like automatically inferring where `typeCast` needs to be > placed (indeed, at the Core level there is a construct for casting by an > equality proof, which plays much the same role). > > Hope this helps, > > Adam > > > On 06/12/2018 12:01, Anthony Clayden wrote: > > The (~) constraint syntax is enabled by either `GADTs` or `TypeFamilies` > > language extension. > > > > GADTs/Assoc Data Types/Assoc Type Synonyms/Type Families arrived in a > > series of papers 2005 to 2008, and IIRC the development wasn't finished > > in full in GHC until after that. (Superclass constraints took up to > > about 2010.) > > > > Suppose I wanted just the (~) parts of those implementations. Which > > would be the best place to look? (The Users Guide doesn't give a > > reference.) ICFP 2008 'Type Checking with Open Type Functions' shows > > uses of (~) in user-written code, but doesn't explain it or motivate it > > as a separate feature. > > > > My specific question is: long before (~), it was possible to write a > > TypeCast class, with bidirectional FunDeps to improve each type > > parameter from the other. But for the compiler to see the type > > improvement at term level, typically you also need a typeCast method and > > to explicitly wrap a term in it. If you just wrote a term of type `a` in > > a place where `b` was wanted, the compiler would either fail to see your > > `TypeCast a b`, or unify the two too eagerly, then infer an overall type > > that wasn't general enough. > > > > (For that reason, the instance for TypeCast goes through some > > devious/indirect other classes/instances or exploits separate > > compilation, to hide what's going on from the compiler's enthusiasm.) > > > > But (~) does some sort of magic: it's a kinda typeclass but without a > > method. How does it mesh with type improvement in the goldilocks zone: > > neither too eager nor too lazy? > > > > > > AntC > > >
_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users