Opened 18 months ago

Closed 18 months ago

Last modified 16 months ago

#14993 closed task (fixed)

QuantifiedConstraints and principal types

Reported by: Iceland_jack Owned by:
Priority: normal Milestone:
Component: Compiler Version: 8.5
Keywords: QuantifiedConstraints Cc:
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 (last modified by Iceland_jack)

This is not a bug but I am trying to understand the implication significance of -XQuantifiedConstraints.

OutsideIn(X) (section 2.4) tells us test actually has a principal type when we have implication constraints)

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

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

Change History (10)

comment:1 Changed 18 months ago 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.

Last edited 18 months ago by Iceland_jack (previous) (diff)

comment:2 Changed 18 months ago by simonpj

In principle yes, but in the wip/T2893 branch:

  • I deliberately never infer a type with quantified constraints. It seems too easy to infer an elaborate, incomprehensible, and perhaps even insoluble, constraint when all that happened was a simple error on the programmer's part.
  • The design deliberately has cls tys or tyvar tys after the => of a quantified constraint; not a ~ Bool. There are too many other ways to solve equalities!
Last edited 18 months ago by simonpj (previous) (diff)

comment:3 Changed 18 months ago 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?

comment:4 Changed 18 months ago by Iceland_jack

It accepts them all (type family example needs some cleverness) Edit: details

Last edited 18 months ago by Iceland_jack (previous) (diff)

comment:5 Changed 18 months ago by Iceland_jack

Description: modified (diff)

comment:6 Changed 18 months ago by AntC

I'd like to ask Simon a 'History of Haskell' type question while this development work is fresh in memory:

The attention it gets in OutsideIn(X) shows the idea has stayed in the back of your mind since 2000. ghc's type inference engine gets radical surgery every half-decade or so.

Did something happen that got -XQuantifiedConstraints to a 'sweet spot'?/changed 4.2's evaluation as it being "not practical"? Or could it as easily have been developed in 2005 or 2010 or ...?

Last edited 18 months ago by AntC (previous) (diff)

comment:7 Changed 18 months ago 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.

comment:8 Changed 18 months ago by Iceland_jack

Resolution: fixed
Status: newclosed

Thanks for the feedback! I am/was interested in any thoughts (not just inference as I seem to have emphasized), closing :)

comment:9 in reply to:  7 Changed 18 months ago by AntC

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

comment:10 Changed 16 months ago by RyanGlScott

Keywords: wipT2893 removed
Note: See TracTickets for help on using tickets.