Opened 18 months ago

Closed 18 months ago

Last modified 16 months ago

#14942 closed bug (invalid)

QuantifiedConstraints: GHC can't infer

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

This works

{-# Language QuantifiedConstraints, GADTs, KindSignatures, RankNTypes, ConstraintKinds #-}

import Data.Kind

newtype Free :: (Type -> Constraint) -> (Type -> Type) where
  Free :: (forall x. cls x => (a -> x) -> x) -> Free cls a

var :: a -> Free cls a
var a = Free $ \var -> 
  var a

oneTwo :: (forall x. semi x => Semigroup x) => Free semi Int
oneTwo = Free $ \var -> 
  var 1 <> var 2

nil :: (forall x. mon x => Monoid x) => Free mon Int
nil = Free $ \var -> 
  mempty

together :: (forall x. mon x => Monoid x) => [Free mon Int]
together = [var 0, nil, oneTwo]

If we comment out together's type signature GHC cannot infer it back, shouldn't it be able to though?

$ ./ghc-stage2 --interactive -ignore-dot-ghci Proposal.hs 
GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( Proposal.hs, interpreted )

Proposal.hs:21:20: error:
    • Could not deduce (Monoid x) arising from a use of ‘nil’
      from the context: cls x
        bound by a quantified context at Proposal.hs:21:1-31
      Possible fix: add (Monoid x) to the context of a quantified context
    • In the expression: nil
      In the expression: [var 0, nil, oneTwo]
      In an equation for ‘together’: together = [var 0, nil, oneTwo]
   |
21 | together = [var 0, nil, oneTwo]
   |                    ^^^

Proposal.hs:21:25: error:
    • Could not deduce (Semigroup x) arising from a use of ‘oneTwo’
      from the context: cls x
        bound by a quantified context at Proposal.hs:21:1-31
      Possible fix:
        add (Semigroup x) to the context of a quantified context
    • In the expression: oneTwo
      In the expression: [var 0, nil, oneTwo]
      In an equation for ‘together’: together = [var 0, nil, oneTwo]
   |
21 | together = [var 0, nil, oneTwo]
   |                         ^^^^^^
Failed, no modules loaded.
Prelude> 

Change History (2)

comment:1 Changed 18 months ago by simonpj

Resolution: invalid
Status: newclosed

If we comment out together's type signature GHC cannot infer it back, shouldn't it be able to though?

No, that's by design. Currently GHC makes no attempt to infer a type with a quantified constraint. It's not impossible to do so -- even fairly easy -- but I worry that they'd then pop up unexpectedly in programs where there was simply a type error.

For now, write a type signature; but re-raise it if that seems to be becoming onerous.

comment:2 Changed 16 months ago by RyanGlScott

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