Skip to content

Cannot sign an expression with its inferred type (or any type at all).

Summary

I have designed a polymorphic expression that GHC can infer the type of, but cannot type even with that very type. I have evidence that the computation expressed by this expression does work. I asked around but no one has come forward with an explanation of the issue so far. Halp.

Steps to reproduce

  1. Get the code by this link. At this time I do not have a smaller example.
  2. Load it in ghci.
  3. Check out :type deasilsB . deasilsA.
  4. Try deasils = deasilsB . deasilsA.

Expected behavior

deasils is assigned the expression deasilsB . deasilsA with the type as inferred. Or else, the assignment is accepted with the type signature such as in the definition found commented out in the source code.

Actual behaviour

See long error.
% ghci-9.2.2 Squeeze.hs
GHCi, version 9.2.2: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/kindaro/code/dotfiles/ghci.conf
[1 of 1] Compiling Main             ( Squeeze.hs, interpreted )
Ok, one module loaded.
λ :reload
[1 of 1] Compiling Main             ( Squeeze.hs, interpreted )
Ok, one module loaded.
λ :type deasilsB . deasilsA
deasilsB . deasilsA
  :: (ForAll peels Functor,
      Squeezy'
        seed
        (Dress seed peels)
        peels
        (Strip seed (Dress seed peels) == '[]),
      Squeezy'
        (seed, value)
        (Dress (seed, value) peels)
        peels
        (Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
     (Dress seed peels, value) -> Dress (seed, value) peels
λ deasils = deasilsB . deasilsA

<interactive>:3:1: error:
    • Could not deduce: Dress seed0 peels0 ~ Dress seed peels
      from the context: (ForAll peels Functor,
                         Squeezy'
                           seed
                           (Dress seed peels)
                           peels
                           (Strip seed (Dress seed peels) == '[]),
                         Squeezy'
                           (seed, value)
                           (Dress (seed, value) peels)
                           peels
                           (Strip (seed, value) (Dress (seed, value) peels) == '[]))
        bound by the inferred type for ‘deasils’:
                   forall {peels :: [* -> *]} {seed} {value}.
                   (ForAll peels Functor,
                    Squeezy'
                      seed
                      (Dress seed peels)
                      peels
                      (Strip seed (Dress seed peels) == '[]),
                    Squeezy'
                      (seed, value)
                      (Dress (seed, value) peels)
                      peels
                      (Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
                   (Dress seed peels, value) -> Dress (seed, value) peels
        at <interactive>:3:1-29
      Expected: (Dress seed peels, value) -> Dress (seed, value) peels
        Actual: (Dress seed0 peels0, value)
                -> Dress (seed0, value) peels0
      NB: ‘Dress’ is a non-injective type family
      The type variables ‘seed0’, ‘peels0’ are ambiguous
    • In the ambiguity check for the inferred type for ‘deasils’
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      When checking the inferred type
        deasils :: forall {peels :: [* -> *]} {seed} {value}.
                   (ForAll peels Functor,
                    Squeezy'
                      seed
                      (Dress seed peels)
                      peels
                      (Strip seed (Dress seed peels) == '[]),
                    Squeezy'
                      (seed, value)
                      (Dress (seed, value) peels)
                      peels
                      (Strip (seed, value) (Dress (seed, value) peels) == '[])) =>
                   (Dress seed peels, value) -> Dress (seed, value) peels

Environment

  • GHC version used: 8.10.7, 9.2.2.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information