#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
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.
It's intriguing -- I never expected people to explore the outer limits of quantified constraints so rapidly. I hope that means that they are 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