#14993: QuantifiedConstraints and principal types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Keywords: | Operating System: Unknown/Multiple QuantifiedConstraints, wipT2893 | Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This is not a bug but I am trying to understand the ~~implication~~ significance of `-XQuantifiedConstraints`. [https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/jfp- outsidein.pdf OutsideIn(X)] (section **2.4**) tells us `test` actually has a principle type when we have implication constraints) {{{#!hs data T :: Type -> Type where T1 :: Int -> T Bool T2 :: T a test :: (a~Bool => b~Bool) => T a -> b -> b test (T1 n) _ = n > 0 test T2 r = r }}} that subsumes {{{#!hs test1 :: T a -> a -> a test1 = test test2 :: T a -> Bool -> Bool test2 = test }}} Now that we have `-XQuantifiedConstraints` does this change the story at all, if not you can close this.. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14993 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler