Opened 6 years ago

Closed 5 years ago

#8913 closed bug (fixed)

either bug or confusing error message mixing PolyKinds and TypeFamilies

Reported by: ghorn Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.1-rc2
Keywords: PolyKinds, TypeFamilies Cc: gregmainland@…, mail@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: indexed_types/should_compile/T8913
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

I found this when using GHC.Generics, but it has to do with TypeFamilies so here is a stand-alone example:

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE PolyKinds #-}

module Test where

class GCat f where
  gcat :: f p -> Int

cat :: (GCat (MyRep a), MyGeneric a) => a -> Int
cat x = gcat (from x)

class MyGeneric a where
  type MyRep a :: * -> *
  from :: a -> (MyRep a) p

This code gives the error message

src/Dyno/Test.hs:12:9:
    Could not deduce (GCat (MyRep a)) arising from a use of ‘gcat’
    from the context (GCat (MyRep a), MyGeneric a)
      bound by the type signature for
                 cat :: (GCat (MyRep a), MyGeneric a) => a -> Int
      at src/Dyno/Test.hs:11:8-48
    In the expression: gcat (from x)
    In an equation for ‘cat’: cat x = gcat (from x)
Failed, modules loaded: none.

If this is not a bug then error message is pretty confusing because it's saying "Can't deduce (C a) from (C a)", where the message I'm used to is "Can't derive (C a) from (C a0)" or something that indicates the mismatch.

Change History (7)

comment:1 Changed 6 years ago by kosmikus

Cc: mail@… added

comment:2 Changed 6 years ago by goldfire

With -fprint-explicit-kinds we see that this really looks like a proper inference bug:

    Could not deduce (GCat * (MyRep a)) arising from a use of ‘gcat’
    from the context (GCat * (MyRep a), MyGeneric a)
      bound by the type signature for
                 cat :: (GCat * (MyRep a), MyGeneric a) => a -> Int
      at Scratch.hs:12:8-48
    In the expression: gcat (from x)
    In an equation for ‘cat’: cat x = gcat (from x)

comment:3 Changed 6 years ago by ghorn

A workaround for this is to put the "GCat" class in its own module (without PolyKinds), and make orphan instances of it where needed (with PolyKinds).

comment:4 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

In c89c57e3b72a8f3de9f35e1bd6e0f70d2b18a941/ghc:

For equalities with incompatible kinds, new IrredCan goes in the inert set, not work list

This change makes the code for canIrred markedly simpler (and more efficient)
See Note [Equalities with incompatible kinds].

I don't think there was really a bug here, but I came across it when
fixing Trac #8913

comment:5 Changed 5 years ago by Simon Peyton Jones <simonpj@…>

In 6ae678e31a5fdd3b0bd1f8613fe164012bb630f4/ghc:

Flattener preserves synonyms, rewriteEvidence can drop buggy "optimisation"

There was a special case in rewriteEvidence, looking like:
  = return (Just (if ctEvPred old_ev `tcEqType` new_pred
                  then old_ev
                  else old_ev { ctev_pred = new_pred }))

But this was wrong: old_pred and new_pred might differ in the kind
of a TyVar occurrence, in which case tcEqType would not notice,
but we really, really want new_pred.  This caused Trac #8913.

I solved this by dropping the whole test, and instead making
the flattener preserve type synonyms. This was easy because
TcEvidence has TcTyConAppCo which (unlike) Coercion, handles
synonyms.

comment:6 Changed 5 years ago by simonpj

Status: newmerge
Test Case: indexed_types/should_compile/T8913

comment:7 Changed 5 years ago by thoughtpolice

Resolution: fixed
Status: mergeclosed

Merged.

Note: See TracTickets for help on using tickets.