#15359: Quantified constraints do not work with equality constraints -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by AntC): Replying to [comment:8 goldfire]: [replying in two instalments]
All the examples in comment:7 involve superclass constraints,
... because your ticket:15351#comment:5 tells me I don't even need instances declared.
mostly on classes without any methods. This is interesting for type- level programming,
Yes the `And` example is for type-level programming. You haven't said those superclass constraints are redundant. Those implications/equalities can be derived from examining the instances; but a) needs reasoning from `Bool` being a closed type, b) needs reasoning from a closed set of instances.
but it's not clear where (even in type-level programming) the rubber is hitting the road here.
I don't expect GHC to be a general-purpose logic engine, so if we want type improvement per David's ghc-devs message "Reasoning backwards" -- which seem eminently sensible, and improvements not achievable by injective Type Families (yet), why ''can't'' I use `QuantifiedConstraints` superclass? I could use similar for "Reasoning backwards" in type-level arithmetic over `Nat`: if a sum is `Z`, both arguments must be `Z`. As I said in comment:3, if it can't use `~`, there's plenty of ways to user-define an equivalent. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15359#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler