QuantifiedConstraints: GHC can't deduce (() :: Constraint)?

{-# Language QuantifiedConstraints, RankNTypes, PolyKinds, ConstraintKinds, UndecidableInstances, GADTs #-}

import Data.Kind

data Dict c where
  Dict :: c => Dict c

class    (a => b) => Implies a b
instance (a => b) => Implies a b

type a :- b = Dict (Implies a b)

iota :: (Implies () a) :- a
iota = Dict

GHC claims that it can't deduce (() :: Constraint) :)

GHCi, version 8.5.20180128: http://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( /tmp/H.hs, interpreted )

/tmp/H.hs:14:8: error:
    • Could not deduce () :: Constraint arising from a use of ‘Dict’
      from the context: Implies () :: Constraint a
        bound by a quantified context at /tmp/H.hs:1:1
      Possible fix:
        add () :: Constraint to the context of
          the type signature for:
            iota :: forall (a :: Constraint). Implies () :: Constraint a :- a
    • In the expression: Dict
      In an equation for ‘iota’: iota = Dict
   |
14 | iota = Dict
   |        ^^^^
Failed, no modules loaded.
Prelude> 

Trac metadata

Trac field	Value
Version	8.5
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture