#14993: QuantifiedConstraints and principal types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 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 Iceland_jack): Namely does this comment still hold

We have ourselves flirted with quantifying over (implication) constraint schemes, but we will argue in 4.2 that this is not practical.

-- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14993#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14993: QuantifiedConstraints and principal types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 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): Aha! I'd forgotten OutsideIn(X) entertains implication constraints. If you're looking for explanation/documentation, section **4.2.1** (starting "costs to the programmer", "costs to the type inference engine") explain the rationale, and it still stands. Simon's saying quantified constraints must be explicitly given by a signature, never inferred. That's in line with many exotic type system features; and makes perfect sense. Would be worth testing the examples from section **2.4** by giving an explicit signature same as what the paper says would be inferred. Does that get `-XQuantifiedConstraints` to accept them? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14993#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14993: QuantifiedConstraints and principal types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Description changed by Iceland_jack: Old description:

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..

New description: 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 principal 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#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14993: QuantifiedConstraints and principal types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: | Keywords: | QuantifiedConstraints, wipT2893 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 simonpj): The big thing that changed in the implementation was when we first had a separate "constraint solver" including implication constraints. I can't quite remember when we first instituted that, but some Git history mining might tell us. That made quantified constraints vastly easier. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14993#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14993: QuantifiedConstraints and principal types -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.5 Resolution: fixed | Keywords: | QuantifiedConstraints, wipT2893 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:7 simonpj]:

a separate "constraint solver" including implication constraints.

Thanks Simon. JFP06 ''Understanding FunDeps via Constraint Handling Rules'' is where the theoretical groundwork was laid, but there was no corresponding development at that time, AFAICT. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14993#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler