No skolem info panic
I've been toying with some type-level lenses and running into some issues with kind unification, when I ran into a panic:
bug.hs:30:34: error:ghc.exe: panic! (the 'impossible' happened)
(GHC version 8.6.2 for x86_64-unknown-mingw32):
No skolem info:
[k_a1Hgj]
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler\utils\Outputable.hs:1160:37 in ghc:Outputable
pprPanic, called at compiler\\typecheck\\TcErrors.hs:2891:5 in ghc:TcErrors
Here's a boiled down version (with a bit of extraneous code left in for context, as it's so short):
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
data Optic a where
--Index :: Nat -> Optic a
--Name :: Symbol -> Optic a
(:.:) :: Optic a -> Optic b -> Optic a -- composition
class Gettable a (optic :: Optic a) where
type Get a (optic :: Optic a)
{-
some basic instances, e.g.
instance Gettable (a,b) (Index 0) where
type Get (a,b) (Index 0) = a
...
-}
instance forall a b (g1 :: Optic a) (g2 :: Optic b).
( Gettable a g1
, b ~ Get a g1
, Gettable b g2
) => Gettable a (g1 :.: g2) where
type Get a (g1 :.: g2) = Get a g2
The program I am actually trying to write has the instance declaration changed to
instance forall a b (g1 :: Optic a) (g2 :: Optic (Get a g1)).
( Gettable a g1
, b ~ Get a g1
, Gettable b g2
) => Gettable a (g1 :.: g2) where
type Get a (g1 :.: g2) = Get (Get a g1) g2
but GHC complains that it can't match kinds:
• Expected kind ‘Optic b’, but ‘g2’ has kind ‘Optic (Get a g1)’
• In the second argument of ‘Gettable’, namely ‘g2’
In the instance declaration for ‘Gettable a (g1 :.: g2)’
|
20 | , Gettable b g2
|
I don't know if there is a way around that, and I'd be interested to hear any advice.
Trac metadata
Trac field | Value |
---|---|
Version | 8.6.2 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |