#15351: QuantifiedConstraints ignore FunctionalDependencies -------------------------------------+------------------------------------- Reporter: aaronvargo | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.5 checker) | Keywords: Resolution: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:6 simonpj]:
Yes, you are right.
Sorry to be dumb, but who is 'you' and which bit are they 'right' about?
It's worth reading the original paper
It's intriguing -- I never expected people to explore the outer limits of quantified constraints so rapidly. I hope that means that they are
Yes I've pored over both your 2000 paper with Ralf, and the hs 2017 more detailed logic. (Both linked from the github proposal.) I didn't see any examples without a `=>` implication; I didn't see any examples without any instances declared at all. And the github proposal didn't mention such possibilities either. proving useful (when not so close to the limits). Is that so? I think this extension is going to be huge -- and that was assuming the implications are needed. Experiments I will try when I get my hands on it: * subsuming quasi-injective logic {{{ class ( (b1 ~ True, b2 ~ True) => res ~ True, res ~ True => b1 ~ True, res ~ True => b2 ~ True, (res ~ False, b1 ~ True) => b2 ~ False, (res ~ False, b2 ~ True) => b1 ~ False ) => And (b1 :: Bool) (b2 :: Bool) ( res :: Bool) }}} * subsuming FunDeps {{{ class (forall b'. C a b' => b' ~ b) -- replicates GHC's "bogus" FD consistency check ref Trac #10675 => C a b where ... -- don't need | a -> b }}} (Is there any way to get a 'strict' after substitution `b'` equal type `b` consistency check?) * maybe subsuming overlap logic/apartness guards (of course more interesting uses than this example) {{{ class ( e ~ e' => d ~ Z, e /~ e' => d ~ (S d'), FindElem e l' d') => FindElemPosn e '( e' ': l' ) (d :: Nat) where ... }}} * field presence/absence for record extension/projection {{{ class ( (forall l a. HasField r1 l a => HasField r3 l a), (forall l a. HasField r2 l a => HasField r3 l a) ) => Merge r1 r2 r3 class ( (forall l a. HasField r3 l a => HasField r1 l a), (forall l a a'. (HasField r1 l a, HasField r2 l a') => HasField r3 l a), (forall l. Lacks r2 l => Lacks r3 l) ) => Project r1 r2 r3 }}} (Apologies for poaching on @aaron's ticket: you're welcome to try the above ideas.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15351#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler