#16123: QuantifiedConstraints fails to deduce trivial constraint -------------------------------------+------------------------------------- Reporter: eschnett | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.6.3 Resolution: duplicate | Keywords: | QuantifiedConstraints Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #14680 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by eschnett): For the record: I have a working work-around using {{{Data.Constraint}}}. The {{{functor}}} class then reads {{{ -- | A functor class (Category (Dom f), Category (Cod f)) => Functor f where -- | Prove that this functor maps from its domain to its codomain proveFunctor :: Ok (Dom f) a => Ok (Dom f) a :- Ok (Cod f) (f a) type Dom f :: CatKind type Cod f :: CatKind fmap :: (Ok (Dom f) a, Ok (Dom f) b) => Dom f a b -> Cod f (f a) (f b) }}} and the previously-failing instance declaration becomes {{{ instance (Functor f, Dom f ~ NFun, Cod f ~ NFun) => Functor (NIdF f) where type Dom (NIdF f) = Dom f type Cod (NIdF f) = Cod f proveFunctor :: forall a. Ok (Dom (NIdF f)) a => Ok (Dom (NIdF f)) a :- Ok (Cod (NIdF f)) ((NIdF f) a) proveFunctor = Sub Dict \\ (proveFunctor @f :: Ok (Dom f) a :- Ok (Cod f) (f a)) fmap f = NFun \(NIdF xs) -> NIdF (neval (fmap f) xs) }}} The disadvantage is that {{{proveFunctor}}} is now an explicit function, and using {{{fmap}}} now might require calling {{{proveFunctor}}} explicitly to invoke it as proof. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/16123#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler