Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mention the result in the error message for JoinKinds #460

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

arybczak
Copy link
Collaborator

Fixes #453.

I avoided any fancy tricks to make it appear only if m is concrete for simplicity.

@arybczak arybczak force-pushed the more-verbose-joinkinds-error branch from 5fcc03f to ab4c027 Compare May 20, 2022 14:31
@arybczak arybczak force-pushed the more-verbose-joinkinds-error branch from ab4c027 to 306f64a Compare May 20, 2022 14:39
@arybczak
Copy link
Collaborator Author

The doctest error is utterly bizarre.

src/Optics.hs:540: failure in expression `:t mapped % folded'
expected: ...
          ...A_Setter cannot be composed with A_Fold
          ...
 but got: mapped % folded
            :: ((TypeError ...), Functor f1, Foldable f2) =>
               Optic m '[] (f1 (f2 b)) (f1 (f2 b)) b b
           ^

Looks like another TypeError GHC quirk 😞

@adamgundry
Copy link
Member

That is bizarre. It looks like GHC is successfully inferring a type for mapped % folded, albeit one that includes a TypeError, and is then printing the inferred type rather than firing the TypeError. At a guess, perhaps the presence of m in the TypeError makes GHC quantify over the constraint?

@adamgundry
Copy link
Member

The issue seems to be that with the :t command, if the type of the expression is polymorphic, any TypeError constraints are quantified over rather than being reported as errors. For example:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

import GHC.TypeLits

type family F a where
  F a = TypeError (ShowType a)

-- :t plugh reports a type error
plugh :: F Int => Int -> ()
plugh _ = ()

-- :t blah doesn't report a type error
blah :: F a => a -> ()
blah _ = ()

-- :t bloo doesn't report a type error
bloo :: Show (F Int) => a -> ()
bloo _ = ()
GHCi, version 9.2.2: https://www.haskell.org/ghc/  :? for help
[1 of 1] Compiling Main             ( TypeErrorQuantification.hs, interpreted )
Ok, one module loaded.
ghci> :t plugh

<interactive>:1:1: error:
    • Int
    • In the expression: plugh
ghci> plugh

<interactive>:2:1: error:
    • Int
    • In the expression: plugh
      In an equation for ‘it’: it = plugh
ghci> :t blah
blah :: (TypeError ...) => a -> ()
ghci> :t \ (x :: a) -> blah @a
\ (x :: a) -> blah @a :: (TypeError ...) => a -> a -> ()
ghci> :t blah @Int

<interactive>:1:1: error:
    • Int
    • In the expression: blah @Int
ghci> blah

<interactive>:6:1: error:
    • a
    • When checking the inferred type
        it :: forall {a}. (TypeError ...) => a -> ()
ghci> :t bloo
bloo :: Show (TypeError ...) => a -> ()

This seems very inconsistent, and is more motiviation for Unsatisfiable at least. But it might also be worth a GHC ticket for TypeError?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Error message for JoinKinds could mention m
2 participants